Geometry Problems of 48th International Mathematical Olympiad (2007)

Problem 2

Consider five points $A$, $B$, $C$, $D$, $E$ such that $ABCD$ is a parallelogram and $BCED$ is a cyclic quadrilateral. Let $l$ be a line passing through $A$, and let $l$ intersect segment $DC$ and line $BC$ at points $F$ and $G$, respectively. Suppose that $EF$ = $EG$ = $EC$. Prove that $l$ is the bisector of angle $DAB$.

structure EuclidGeom.IMO_2007_2.Setting (P : Type u_1) [EuclidGeom.EuclideanPlane P] : Type u_1

• A : P
• B : P
• C : P
• D : P
• E : P
• hp : { point₁ := s.A, point₂ := s.B, point₃ := s.C, point₄ := s.D }.IsPrgND
• ω : EuclidGeom.Circle P
• hbo : EuclidGeom.lies_on s.B s.ω
• hco : EuclidGeom.lies_on s.C s.ω
• heo : EuclidGeom.lies_on s.E s.ω
• hdo : EuclidGeom.lies_on s.D s.ω
• l : EuclidGeom.Line P
• ha : EuclidGeom.lies_on s.A s.l
• F : P
• hf : EuclidGeom.lies_on s.F s.l
• hfdc : EuclidGeom.lies_int s.F { source := s.D, target := s.C }
• G : P
• hg : EuclidGeom.lies_on s.G s.l
• hglbc : EuclidGeom.lies_on s.G (LIN s.B s.C (_ : { point₁ := s.A, point₂ := s.B, point₃ := s.C, point₄ := s.D }.point₃ ≠ { point₁ := s.A, point₂ := s.B, point₃ := s.C, point₄ := s.D }.point₂))
• hefg : dist s.E s.F = dist s.E s.G
• hegc : dist s.E s.G = dist s.E s.C

instance EuclidGeom.IMO_2007_2.Setting.C_ne_B {P : Type u_1} [EuclidGeom.EuclideanPlane P] (e : EuclidGeom.IMO_2007_2.Setting P) : EuclidGeom.PtNe e.C e.B

$C$ ≠ $B$ since $ABCD$ is a nondegenerate parallelogram.

Equations

• (_ : EuclidGeom.PtNe e.C e.B) = (_ : Fact (e.C ≠ e.B))

instance EuclidGeom.IMO_2007_2.Setting.D_ne_C {P : Type u_1} [EuclidGeom.EuclideanPlane P] (e : EuclidGeom.IMO_2007_2.Setting P) : EuclidGeom.PtNe e.D e.C

$D$ ≠ $C$ since $ABCD$ is a nondegenerate parallelogram.

Equations

• (_ : EuclidGeom.PtNe e.D e.C) = (_ : Fact (e.D ≠ e.C))

instance EuclidGeom.IMO_2007_2.Setting.D_ne_A {P : Type u_1} [EuclidGeom.EuclideanPlane P] (e : EuclidGeom.IMO_2007_2.Setting P) : EuclidGeom.PtNe e.D e.A

$D$ ≠ $A$ since $ABCD$ is a nondegenerate parallelogram.

Equations

• (_ : EuclidGeom.PtNe e.D e.A) = (_ : Fact (e.D ≠ e.A))

instance EuclidGeom.IMO_2007_2.Setting.B_ne_A {P : Type u_1} [EuclidGeom.EuclideanPlane P] (e : EuclidGeom.IMO_2007_2.Setting P) : EuclidGeom.PtNe e.B e.A

$B$ ≠ $A$ since $ABCD$ is a nondegenerate parallelogram.

Equations

• (_ : EuclidGeom.PtNe e.B e.A) = (_ : Fact (e.B ≠ e.A))

instance EuclidGeom.IMO_2007_2.Setting.F_ne_C {P : Type u_1} [EuclidGeom.EuclideanPlane P] (e : EuclidGeom.IMO_2007_2.Setting P) : EuclidGeom.PtNe e.F e.C

$F$ ≠ $C$ since $F$ lies in the interior the segment $DC$.

Equations

• (_ : EuclidGeom.PtNe e.F e.C) = (_ : Fact (e.F ≠ e.C))

def EuclidGeom.IMO_2007_2.Setting.lbc {P : Type u_1} [EuclidGeom.EuclideanPlane P] (e : EuclidGeom.IMO_2007_2.Setting P) : EuclidGeom.Line P

Rename line $BC$ as lbc.

Equations

• e.lbc = LIN e.B e.C (_ : e.C ≠ e.B)

def EuclidGeom.IMO_2007_2.Setting.ldc {P : Type u_1} [EuclidGeom.EuclideanPlane P] (e : EuclidGeom.IMO_2007_2.Setting P) : EuclidGeom.Line P

Rename line $DC$ as ldc.

Equations

• e.ldc = LIN e.D e.C (_ : e.C ≠ e.D)

@[inline, reducible]

abbrev EuclidGeom.IMO_2007_2.Setting.prg {P : Type u_1} [EuclidGeom.EuclideanPlane P] (e : EuclidGeom.IMO_2007_2.Setting P) : EuclidGeom.ParallelogramND P

Rename the nondegenerate parallelogram $ABCD$ as prg.

Equations

• e.prg = EuclidGeom.ParallelogramND.mk_pt_pt_pt_pt e.A e.B e.C e.D (_ : { point₁ := e.A, point₂ := e.B, point₃ := e.C, point₄ := e.D }.IsPrgND)

theorem EuclidGeom.IMO_2007_2.Setting.hbcd {P : Type u_1} [EuclidGeom.EuclideanPlane P] (e : EuclidGeom.IMO_2007_2.Setting P) : ¬EuclidGeom.Collinear e.B e.C e.D

$B$, $C$ and $D$ are not collinear since $ABCD$ is a nondegenerate parallelogram.

theorem EuclidGeom.IMO_2007_2.Setting.hcda {P : Type u_1} [EuclidGeom.EuclideanPlane P] (e : EuclidGeom.IMO_2007_2.Setting P) : ¬EuclidGeom.Collinear e.C e.D e.A

$C$, $D$ and $A$ are not collinear since $ABCD$ is a nondegenerate parallelogram.

theorem EuclidGeom.IMO_2007_2.Setting.habd {P : Type u_1} [EuclidGeom.EuclideanPlane P] (e : EuclidGeom.IMO_2007_2.Setting P) : ¬EuclidGeom.Collinear e.A e.B e.D

$C$, $D$ and $A$ are not collinear since $ABCD$ is a nondegenerate parallelogram.

theorem EuclidGeom.IMO_2007_2.Setting.hblbc {P : Type u_1} [EuclidGeom.EuclideanPlane P] (e : EuclidGeom.IMO_2007_2.Setting P) : EuclidGeom.lies_on e.B e.lbc

$B$ lies on line $BC$.

theorem EuclidGeom.IMO_2007_2.Setting.hclbc {P : Type u_1} [EuclidGeom.EuclideanPlane P] (e : EuclidGeom.IMO_2007_2.Setting P) : EuclidGeom.lies_on e.C e.lbc

$C$ lies on line $BC$.

theorem EuclidGeom.IMO_2007_2.Setting.hdldc {P : Type u_1} [EuclidGeom.EuclideanPlane P] (e : EuclidGeom.IMO_2007_2.Setting P) : EuclidGeom.lies_on e.D e.ldc

$D$ lies on line $DC$.

theorem EuclidGeom.IMO_2007_2.Setting.hcldc {P : Type u_1} [EuclidGeom.EuclideanPlane P] (e : EuclidGeom.IMO_2007_2.Setting P) : EuclidGeom.lies_on e.C e.ldc

$C$ lies on line $DC$.

theorem EuclidGeom.IMO_2007_2.Setting.halab {P : Type u_1} [EuclidGeom.EuclideanPlane P] (e : EuclidGeom.IMO_2007_2.Setting P) : EuclidGeom.lies_on e.A (LIN e.A e.B)

$A$ lies on line $AB$.

theorem EuclidGeom.IMO_2007_2.Setting.hblab {P : Type u_1} [EuclidGeom.EuclideanPlane P] (e : EuclidGeom.IMO_2007_2.Setting P) : EuclidGeom.lies_on e.B (LIN e.A e.B)

$B$ lies on line $AB$.

theorem EuclidGeom.IMO_2007_2.Setting.hdlda {P : Type u_1} [EuclidGeom.EuclideanPlane P] (e : EuclidGeom.IMO_2007_2.Setting P) : EuclidGeom.lies_on e.D (LIN e.D e.A)

$D$ lies on line $DA$.

theorem EuclidGeom.IMO_2007_2.Setting.halda {P : Type u_1} [EuclidGeom.EuclideanPlane P] (e : EuclidGeom.IMO_2007_2.Setting P) : EuclidGeom.lies_on e.A (LIN e.D e.A)

$A$ lies on line $DA$.

theorem EuclidGeom.IMO_2007_2.Setting.hfldc {P : Type u_1} [EuclidGeom.EuclideanPlane P] (e : EuclidGeom.IMO_2007_2.Setting P) : EuclidGeom.lies_on e.F e.ldc

$F$ lies on line $DC$ since $F$ lies in the interior the segment $DC$.

theorem EuclidGeom.IMO_2007_2.Setting.hln {P : Type u_1} [EuclidGeom.EuclideanPlane P] (e : EuclidGeom.IMO_2007_2.Setting P) : e.ldc ≠ e.lbc

Line $DC$ is not equal to line $BC$ since $B$, $C$ and $D$ are not collinear.

theorem EuclidGeom.IMO_2007_2.Setting.hnab {P : Type u_1} [EuclidGeom.EuclideanPlane P] (e : EuclidGeom.IMO_2007_2.Setting P) : e.ldc ≠ LIN e.A e.B

Line $DC$ is not equal to line $AB$ since $A$, $B$ and $D$ are not collinear.

theorem EuclidGeom.IMO_2007_2.Setting.hdan {P : Type u_1} [EuclidGeom.EuclideanPlane P] (e : EuclidGeom.IMO_2007_2.Setting P) : LIN e.D e.A ≠ e.lbc

Line $DC$ is not equal to line $BC$ since $B$, $C$ and $D$ are not collinear.

theorem EuclidGeom.IMO_2007_2.Setting.hdcab {P : Type u_1} [EuclidGeom.EuclideanPlane P] (e : EuclidGeom.IMO_2007_2.Setting P) : EuclidGeom.Parallel e.ldc (LIN e.A e.B)

Line $DC$ is parallel to line $AB$ since $ABCD$ is a nondegenerate parallelogram.

theorem EuclidGeom.IMO_2007_2.Setting.hdabc {P : Type u_1} [EuclidGeom.EuclideanPlane P] (e : EuclidGeom.IMO_2007_2.Setting P) : EuclidGeom.Parallel (LIN e.D e.A) e.lbc

Line $DA$ is parallel to line $BC$ since $ABCD$ is a nondegenerate parallelogram.

instance EuclidGeom.IMO_2007_2.Setting.G_ne_A {P : Type u_1} [EuclidGeom.EuclideanPlane P] (e : EuclidGeom.IMO_2007_2.Setting P) : EuclidGeom.PtNe e.G e.A

$G$ ≠ $A$.

Equations

• (_ : EuclidGeom.PtNe e.G e.A) = (_ : Fact (e.G ≠ e.A))

instance EuclidGeom.IMO_2007_2.Setting.G_ne_F {P : Type u_1} [EuclidGeom.EuclideanPlane P] (e : EuclidGeom.IMO_2007_2.Setting P) : EuclidGeom.PtNe e.G e.F

$G$ ≠ $F$.

Equations

• (_ : EuclidGeom.PtNe e.G e.F) = (_ : Fact (e.G ≠ e.F))

instance EuclidGeom.IMO_2007_2.Setting.G_ne_B {P : Type u_1} [EuclidGeom.EuclideanPlane P] (e : EuclidGeom.IMO_2007_2.Setting P) : EuclidGeom.PtNe e.G e.B

$G$ ≠ $B$.

Equations

• (_ : EuclidGeom.PtNe e.G e.B) = (_ : Fact (e.G ≠ e.B))

instance EuclidGeom.IMO_2007_2.Setting.G_ne_C {P : Type u_1} [EuclidGeom.EuclideanPlane P] (e : EuclidGeom.IMO_2007_2.Setting P) : EuclidGeom.PtNe e.G e.C

$G$ ≠ $C$.

Equations

• (_ : EuclidGeom.PtNe e.G e.C) = (_ : Fact (e.G ≠ e.C))

theorem EuclidGeom.IMO_2007_2.Setting.hefc {P : Type u_1} [EuclidGeom.EuclideanPlane P] (e : EuclidGeom.IMO_2007_2.Setting P) : dist e.E e.F = dist e.E e.C

$|EF| = |EC|$.

theorem EuclidGeom.IMO_2007_2.Setting.hfag {P : Type u_1} [EuclidGeom.EuclideanPlane P] (e : EuclidGeom.IMO_2007_2.Setting P) : EuclidGeom.lies_int e.F { source := e.A, target := e.G }

$F$ lies in the interior the segment $AG$ due to the conditions of parallel lines.

theorem EuclidGeom.IMO_2007_2.Setting.hbcg {P : Type u_1} [EuclidGeom.EuclideanPlane P] (e : EuclidGeom.IMO_2007_2.Setting P) : EuclidGeom.lies_int e.C { source := e.B, target := e.G }

$C$ lies in the interior the segment $BG$ due to the conditions of parallel lines.

instance EuclidGeom.IMO_2007_2.Setting.E_ne_B {P : Type u_1} [EuclidGeom.EuclideanPlane P] (e : EuclidGeom.IMO_2007_2.Setting P) : EuclidGeom.PtNe e.E e.B

$E$ ≠ $B$.

Equations

• (_ : EuclidGeom.PtNe e.E e.B) = (_ : Fact (e.E ≠ e.B))

instance EuclidGeom.IMO_2007_2.Setting.E_ne_C {P : Type u_1} [EuclidGeom.EuclideanPlane P] (e : EuclidGeom.IMO_2007_2.Setting P) : EuclidGeom.PtNe e.E e.C

$E$ ≠ $C$.

Equations

• (_ : EuclidGeom.PtNe e.E e.C) = (_ : Fact (e.E ≠ e.C))

instance EuclidGeom.IMO_2007_2.Setting.E_ne_D {P : Type u_1} [EuclidGeom.EuclideanPlane P] (e : EuclidGeom.IMO_2007_2.Setting P) : EuclidGeom.PtNe e.E e.D

$E$ ≠ $D$.

Equations

• (_ : EuclidGeom.PtNe e.E e.D) = (_ : Fact (e.E ≠ e.D))

theorem EuclidGeom.IMO_2007_2.Setting.hbcde {P : Type u_1} [EuclidGeom.EuclideanPlane P] (e : EuclidGeom.IMO_2007_2.Setting P) : ∡ e.C e.B e.E = ∡ e.C e.D e.E

∠$CBE$ and ∠$CDE$ are congruent modulo π since $BCED$ is a cyclic quadrilateral.

theorem EuclidGeom.IMO_2007_2.Setting.helbc {P : Type u_1} [EuclidGeom.EuclideanPlane P] (e : EuclidGeom.IMO_2007_2.Setting P) : ¬EuclidGeom.lies_on e.E e.lbc

$E$ is not lies on line $BC$.

theorem EuclidGeom.IMO_2007_2.Setting.heldc {P : Type u_1} [EuclidGeom.EuclideanPlane P] (e : EuclidGeom.IMO_2007_2.Setting P) : ¬EuclidGeom.lies_on e.E e.ldc

$E$ is not lies on line $DC$.

theorem EuclidGeom.IMO_2007_2.Setting.hgldc {P : Type u_1} [EuclidGeom.EuclideanPlane P] (e : EuclidGeom.IMO_2007_2.Setting P) : ¬EuclidGeom.lies_on e.G e.ldc

$G$ is not lies on line $DC$.

@[inline, reducible]

abbrev EuclidGeom.IMO_2007_2.Setting.K {P : Type u_1} [EuclidGeom.EuclideanPlane P] (e : EuclidGeom.IMO_2007_2.Setting P) : P

Let $K$ be the midpoint of segment $CG$.

Equations

• e.K = { source := e.C, target := e.G }.midpoint

@[inline, reducible]

abbrev EuclidGeom.IMO_2007_2.Setting.L {P : Type u_1} [EuclidGeom.EuclideanPlane P] (e : EuclidGeom.IMO_2007_2.Setting P) : P

Let $L$ be the midpoint of segment $FC$.

Equations

• e.L = { source := e.F, target := e.C }.midpoint

instance EuclidGeom.IMO_2007_2.Setting.K_ne_B {P : Type u_1} [EuclidGeom.EuclideanPlane P] (e : EuclidGeom.IMO_2007_2.Setting P) : EuclidGeom.PtNe e.K e.B

$K$ ≠ $B$ since it is the midpoint of the nondegenerate segment $CG$.

Equations

• (_ : EuclidGeom.PtNe e.K e.B) = (_ : Fact (e.K ≠ e.B))

instance EuclidGeom.IMO_2007_2.Setting.K_ne_C {P : Type u_1} [EuclidGeom.EuclideanPlane P] (e : EuclidGeom.IMO_2007_2.Setting P) : EuclidGeom.PtNe e.K e.C

$K$ ≠ $C$ since it is the midpoint of the nondegenerate segment $CG$.

Equations

• (_ : EuclidGeom.PtNe e.K e.C) = (_ : Fact (e.K ≠ e.C))

instance EuclidGeom.IMO_2007_2.Setting.L_ne_F {P : Type u_1} [EuclidGeom.EuclideanPlane P] (e : EuclidGeom.IMO_2007_2.Setting P) : EuclidGeom.PtNe e.L e.F

$L$ ≠ $F$ since it is the midpoint of the nondegenerate segment $FC$.

Equations

• (_ : EuclidGeom.PtNe e.L e.F) = (_ : Fact (e.L ≠ e.F))

instance EuclidGeom.IMO_2007_2.Setting.L_ne_C {P : Type u_1} [EuclidGeom.EuclideanPlane P] (e : EuclidGeom.IMO_2007_2.Setting P) : EuclidGeom.PtNe e.L e.C

$L$ ≠ $C$ since it is the midpoint of the nondegenerate segment $FC$.

Equations

• (_ : EuclidGeom.PtNe e.L e.C) = (_ : Fact (e.L ≠ e.C))

instance EuclidGeom.IMO_2007_2.Setting.L_ne_D {P : Type u_1} [EuclidGeom.EuclideanPlane P] (e : EuclidGeom.IMO_2007_2.Setting P) : EuclidGeom.PtNe e.L e.D

$L$ ≠ $D$ since $L$ lies in the interior the segment $DC$.

Equations

• (_ : EuclidGeom.PtNe e.L e.D) = (_ : Fact (e.L ≠ e.D))

theorem EuclidGeom.IMO_2007_2.Setting.hkp {P : Type u_1} [EuclidGeom.EuclideanPlane P] (e : EuclidGeom.IMO_2007_2.Setting P) : e.K = EuclidGeom.perp_foot e.E e.lbc

$K$ is the perpendicular foot from $E$ to line $BC$.

theorem EuclidGeom.IMO_2007_2.Setting.hlp {P : Type u_1} [EuclidGeom.EuclideanPlane P] (e : EuclidGeom.IMO_2007_2.Setting P) : e.L = EuclidGeom.perp_foot e.E e.ldc

$L$ is the perpendicular foot from $E$ to line $DC$.

theorem EuclidGeom.IMO_2007_2.Setting.hklbc {P : Type u_1} [EuclidGeom.EuclideanPlane P] (e : EuclidGeom.IMO_2007_2.Setting P) : EuclidGeom.lies_on e.K e.lbc

$K$ lies on line $BC$ since it is the perpendicular foot from $E$ to line $BC$.

theorem EuclidGeom.IMO_2007_2.Setting.hlldc {P : Type u_1} [EuclidGeom.EuclideanPlane P] (e : EuclidGeom.IMO_2007_2.Setting P) : EuclidGeom.lies_on e.L e.ldc

$L$ lies on line $DC$ since it is the perpendicular foot from $E$ to line $DC$.

def EuclidGeom.IMO_2007_2.Setting.KBE {P : Type u_1} [EuclidGeom.EuclideanPlane P] (e : EuclidGeom.IMO_2007_2.Setting P) : EuclidGeom.TriangleND P

Rename nondegenerate ▵$KBE$ as KBE.

Equations

• e.KBE = { val := { point₁ := e.K, point₂ := e.B, point₃ := e.E }, property := (_ : ¬EuclidGeom.Collinear e.K e.B { point₁ := e.K, point₂ := e.B, point₃ := e.E }.point₃) }

def EuclidGeom.IMO_2007_2.Setting.LDE {P : Type u_1} [EuclidGeom.EuclideanPlane P] (e : EuclidGeom.IMO_2007_2.Setting P) : EuclidGeom.TriangleND P

Rename nondegenerate ▵$LDE$ as LDE.

Equations

• e.LDE = { val := { point₁ := e.L, point₂ := e.D, point₃ := e.E }, property := (_ : ¬EuclidGeom.Collinear e.L e.D { point₁ := e.L, point₂ := e.D, point₃ := e.E }.point₃) }

def EuclidGeom.IMO_2007_2.Setting.KCE {P : Type u_1} [EuclidGeom.EuclideanPlane P] (e : EuclidGeom.IMO_2007_2.Setting P) : EuclidGeom.TriangleND P

Rename nondegenerate ▵$KCE$ as KCE.

Equations

• e.KCE = { val := { point₁ := e.K, point₂ := e.C, point₃ := e.E }, property := (_ : ¬EuclidGeom.Collinear e.K e.C { point₁ := e.K, point₂ := e.C, point₃ := e.E }.point₃) }

def EuclidGeom.IMO_2007_2.Setting.LCE {P : Type u_1} [EuclidGeom.EuclideanPlane P] (e : EuclidGeom.IMO_2007_2.Setting P) : EuclidGeom.TriangleND P

Rename nondegenerate ▵$LCE$ as LCE.

Equations

• e.LCE = { val := { point₁ := e.L, point₂ := e.C, point₃ := e.E }, property := (_ : ¬EuclidGeom.Collinear e.L e.C { point₁ := e.L, point₂ := e.C, point₃ := e.E }.point₃) }

theorem EuclidGeom.IMO_2007_2.ratio_eq {P : Type u_1} [EuclidGeom.EuclideanPlane P] (e : EuclidGeom.IMO_2007_2.Setting P) : dist e.E e.K / dist e.E e.L = dist e.K e.C / dist e.L e.C

$|EK| / |EL| = |KC| / |LC|$.

theorem EuclidGeom.IMO_2007_2.tri_CGF_isIsoceles {P : Type u_1} [EuclidGeom.EuclideanPlane P] (e : EuclidGeom.IMO_2007_2.Setting P) : EuclidGeom.Triangle.IsIsoceles { point₁ := e.C, point₂ := e.G, point₃ := e.F }

▵$CGF$ is a isosceles triangle.

theorem EuclidGeom.IMO_2007_2.Result {P : Type u_1} [EuclidGeom.EuclideanPlane P] (e : EuclidGeom.IMO_2007_2.Setting P) : EuclidGeom.IsAngBisLine (ANG e.D e.A e.B) e.l

$l$ is the bisector of angle $DAB$.