IMO 2019 Q2

In triangle ABC, point A₁ lies on side BC and point B₁ lies on side AC. Let P and Q be points on segments AA₁ and BB₁, respectively, such that PQ is parallel to AB. Let P₁ be a point on line PB₁, such that B₁ lies strictly between P and P₁, and ∠PP₁C = ∠BAC. Similarly, let Q₁ be a point on line QA₁, such that A₁ lies strictly between Q and Q₁, and ∠CQ₁Q = ∠CBA.

Prove that points P, Q, P₁, and Q₁ are concyclic.

We follow Solution 1 from the official solutions. Letting the rays AA₁ and BB₁ intersect the circumcircle of ABC at A₂ and B₂ respectively, we show with an angle chase that P, Q, A₂, B₂ are concyclic and let ω be the circle through those points. We then show that C, Q₁, A₂, A₁ are concyclic, and then that Q₁ lies on ω, and similarly that P₁ lies on ω, so the required four points are concyclic.

Note that most of the formal proof is actually proving nondegeneracy conditions needed for that angle chase / concyclicity argument, where an informal solution doesn't discuss those conditions at all. Also note that (as described in Geometry.Euclidean.Angle.Oriented.Basic) the oriented angles used are modulo 2 * π, so parts of the angle chase that are only valid for angles modulo π (as used in the informal solution) are represented as equalities of twice angles, which we write as (2 : ℤ) • ∡ _ _ _ = (2 : ℤ) • ∡ _ _ _.

structure Imo2019Q2.Imo2019q2Cfg (V : Type u_1) (Pt : Type u_2) [NormedAddCommGroup V] [InnerProductSpace Real V] [MetricSpace Pt] [NormedAddTorsor V Pt] : Type u_2

A configuration satisfying the conditions of the problem. We define this structure to avoid passing many hypotheses around as we build up information about the configuration; the final result for a statement of the problem not using this structure is then deduced from one in terms of this structure.

• A : Pt
• B : Pt
• C : Pt
• A₁ : Pt
• B₁ : Pt
• P : Pt
• Q : Pt
• P₁ : Pt
• Q₁ : Pt
• affineIndependent_ABC : AffineIndependent Real (Matrix.vecCons self.A (Matrix.vecCons self.B (Matrix.vecCons self.C Matrix.vecEmpty)))
• wbtw_B_A₁_C : Wbtw Real self.B self.A₁ self.C
• wbtw_A_B₁_C : Wbtw Real self.A self.B₁ self.C
• wbtw_A_P_A₁ : Wbtw Real self.A self.P self.A₁
• wbtw_B_Q_B₁ : Wbtw Real self.B self.Q self.B₁
• PQ_parallel_AB : (affineSpan Real (Insert.insert self.P (Singleton.singleton self.Q))).Parallel (affineSpan Real (Insert.insert self.A (Singleton.singleton self.B)))
• P_ne_Q : Ne self.P self.Q
• sbtw_P_B₁_P₁ : Sbtw Real self.P self.B₁ self.P₁
• angle_PP₁C_eq_angle_BAC : Eq (EuclideanGeometry.angle self.P self.P₁ self.C) (EuclideanGeometry.angle self.B self.A self.C)
• C_ne_P₁ : Ne self.C self.P₁
• sbtw_Q_A₁_Q₁ : Sbtw Real self.Q self.A₁ self.Q₁
• angle_CQ₁Q_eq_angle_CBA : Eq (EuclideanGeometry.angle self.C self.Q₁ self.Q) (EuclideanGeometry.angle self.C self.B self.A)
• C_ne_Q₁ : Ne self.C self.Q₁

def Imo2019Q2.someOrientation (V : Type u_1) [NormedAddCommGroup V] [InnerProductSpace Real V] [hd2 : Fact (Eq (Module.finrank Real V) 2)] : Module.Oriented Real V (Fin 2)

A default choice of orientation, for lemmas that need to pick one.

Equations

• Eq (Imo2019Q2.someOrientation V) { positiveOrientation := (Module.finBasisOfFinrankEq Real V ⋯).orientation }

def Imo2019Q2.Imo2019q2Cfg.symm {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace Real V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019q2Cfg V Pt) : Imo2019q2Cfg V Pt

The configuration has symmetry, allowing results proved for one point to be applied for another (where the informal solution says "similarly").

Equations

• One or more equations did not get rendered due to their size.

Configuration properties that are obvious from the diagram, and construction of the

points A₂ and B₂

theorem Imo2019Q2.Imo2019q2Cfg.A_ne_B {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace Real V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019q2Cfg V Pt) : Ne cfg.A cfg.B

theorem Imo2019Q2.Imo2019q2Cfg.A_ne_C {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace Real V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019q2Cfg V Pt) : Ne cfg.A cfg.C

theorem Imo2019Q2.Imo2019q2Cfg.B_ne_C {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace Real V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019q2Cfg V Pt) : Ne cfg.B cfg.C

theorem Imo2019Q2.Imo2019q2Cfg.not_collinear_ABC {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace Real V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019q2Cfg V Pt) : Not (Collinear Real (Insert.insert cfg.A (Insert.insert cfg.B (Singleton.singleton cfg.C))))

def Imo2019Q2.Imo2019q2Cfg.triangleABC {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace Real V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019q2Cfg V Pt) : Affine.Triangle Real Pt

ABC as a Triangle.

Equations

• Eq cfg.triangleABC { points := Matrix.vecCons cfg.A (Matrix.vecCons cfg.B (Matrix.vecCons cfg.C Matrix.vecEmpty)), independent := ⋯ }

theorem Imo2019Q2.Imo2019q2Cfg.A_mem_circumsphere {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace Real V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019q2Cfg V Pt) : Membership.mem (Affine.Simplex.circumsphere cfg.triangleABC) cfg.A

theorem Imo2019Q2.Imo2019q2Cfg.B_mem_circumsphere {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace Real V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019q2Cfg V Pt) : Membership.mem (Affine.Simplex.circumsphere cfg.triangleABC) cfg.B

theorem Imo2019Q2.Imo2019q2Cfg.C_mem_circumsphere {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace Real V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019q2Cfg V Pt) : Membership.mem (Affine.Simplex.circumsphere cfg.triangleABC) cfg.C

theorem Imo2019Q2.Imo2019q2Cfg.symm_triangleABC {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace Real V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019q2Cfg V Pt) : Eq cfg.symm.triangleABC (Affine.Simplex.reindex cfg.triangleABC (Equiv.swap 0 1))

theorem Imo2019Q2.Imo2019q2Cfg.symm_triangleABC_circumsphere {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace Real V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019q2Cfg V Pt) : Eq (Affine.Simplex.circumsphere cfg.symm.triangleABC) (Affine.Simplex.circumsphere cfg.triangleABC)

def Imo2019Q2.Imo2019q2Cfg.A₂ {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace Real V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019q2Cfg V Pt) : Pt

A₂ is the second point of intersection of the ray AA₁ with the circumcircle of ABC.

Equations

• Eq cfg.A₂ ((Affine.Simplex.circumsphere cfg.triangleABC).secondInter cfg.A (VSub.vsub cfg.A₁ cfg.A))

def Imo2019Q2.Imo2019q2Cfg.B₂ {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace Real V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019q2Cfg V Pt) : Pt

B₂ is the second point of intersection of the ray BB₁ with the circumcircle of ABC.

Equations

• Eq cfg.B₂ ((Affine.Simplex.circumsphere cfg.triangleABC).secondInter cfg.B (VSub.vsub cfg.B₁ cfg.B))

theorem Imo2019Q2.Imo2019q2Cfg.A₂_mem_circumsphere {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace Real V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019q2Cfg V Pt) : Membership.mem (Affine.Simplex.circumsphere cfg.triangleABC) cfg.A₂

theorem Imo2019Q2.Imo2019q2Cfg.B₂_mem_circumsphere {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace Real V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019q2Cfg V Pt) : Membership.mem (Affine.Simplex.circumsphere cfg.triangleABC) cfg.B₂

theorem Imo2019Q2.Imo2019q2Cfg.symm_A₂ {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace Real V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019q2Cfg V Pt) : Eq cfg.symm.A₂ cfg.B₂

theorem Imo2019Q2.Imo2019q2Cfg.QP_parallel_BA {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace Real V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019q2Cfg V Pt) : (affineSpan Real (Insert.insert cfg.Q (Singleton.singleton cfg.P))).Parallel (affineSpan Real (Insert.insert cfg.B (Singleton.singleton cfg.A)))

theorem Imo2019Q2.Imo2019q2Cfg.A_ne_A₁ {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace Real V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019q2Cfg V Pt) : Ne cfg.A cfg.A₁

theorem Imo2019Q2.Imo2019q2Cfg.collinear_PAA₁A₂ {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace Real V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019q2Cfg V Pt) : Collinear Real (Insert.insert cfg.P (Insert.insert cfg.A (Insert.insert cfg.A₁ (Singleton.singleton cfg.A₂))))

theorem Imo2019Q2.Imo2019q2Cfg.A₁_ne_C {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace Real V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019q2Cfg V Pt) : Ne cfg.A₁ cfg.C

theorem Imo2019Q2.Imo2019q2Cfg.B₁_ne_C {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace Real V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019q2Cfg V Pt) : Ne cfg.B₁ cfg.C

theorem Imo2019Q2.Imo2019q2Cfg.Q_not_mem_CB {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace Real V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019q2Cfg V Pt) : Not (Membership.mem (affineSpan Real (Insert.insert cfg.C (Singleton.singleton cfg.B))) cfg.Q)

theorem Imo2019Q2.Imo2019q2Cfg.Q_ne_B {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace Real V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019q2Cfg V Pt) : Ne cfg.Q cfg.B

theorem Imo2019Q2.Imo2019q2Cfg.sOppSide_CB_Q_Q₁ {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace Real V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019q2Cfg V Pt) : (affineSpan Real (Insert.insert cfg.C (Singleton.singleton cfg.B))).SOppSide cfg.Q cfg.Q₁

Relate the orientations of different angles in the configuration

theorem Imo2019Q2.Imo2019q2Cfg.oangle_CQ₁Q_sign_eq_oangle_CBA_sign {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace Real V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019q2Cfg V Pt) [Module.Oriented Real V (Fin 2)] [Fact (Eq (Module.finrank Real V) 2)] : Eq (EuclideanGeometry.oangle cfg.C cfg.Q₁ cfg.Q).sign (EuclideanGeometry.oangle cfg.C cfg.B cfg.A).sign

theorem Imo2019Q2.Imo2019q2Cfg.oangle_CQ₁Q_eq_oangle_CBA {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace Real V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019q2Cfg V Pt) [Module.Oriented Real V (Fin 2)] [Fact (Eq (Module.finrank Real V) 2)] : Eq (EuclideanGeometry.oangle cfg.C cfg.Q₁ cfg.Q) (EuclideanGeometry.oangle cfg.C cfg.B cfg.A)

More obvious configuration properties

theorem Imo2019Q2.Imo2019q2Cfg.A₁_ne_B {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace Real V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019q2Cfg V Pt) [hd2 : Fact (Eq (Module.finrank Real V) 2)] : Ne cfg.A₁ cfg.B

theorem Imo2019Q2.Imo2019q2Cfg.sbtw_B_A₁_C {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace Real V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019q2Cfg V Pt) [hd2 : Fact (Eq (Module.finrank Real V) 2)] : Sbtw Real cfg.B cfg.A₁ cfg.C

theorem Imo2019Q2.Imo2019q2Cfg.sbtw_A_B₁_C {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace Real V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019q2Cfg V Pt) [hd2 : Fact (Eq (Module.finrank Real V) 2)] : Sbtw Real cfg.A cfg.B₁ cfg.C

theorem Imo2019Q2.Imo2019q2Cfg.sbtw_A_A₁_A₂ {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace Real V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019q2Cfg V Pt) [hd2 : Fact (Eq (Module.finrank Real V) 2)] : Sbtw Real cfg.A cfg.A₁ cfg.A₂

theorem Imo2019Q2.Imo2019q2Cfg.sbtw_B_B₁_B₂ {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace Real V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019q2Cfg V Pt) [hd2 : Fact (Eq (Module.finrank Real V) 2)] : Sbtw Real cfg.B cfg.B₁ cfg.B₂

theorem Imo2019Q2.Imo2019q2Cfg.A₂_ne_A {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace Real V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019q2Cfg V Pt) [hd2 : Fact (Eq (Module.finrank Real V) 2)] : Ne cfg.A₂ cfg.A

theorem Imo2019Q2.Imo2019q2Cfg.A₂_ne_P {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace Real V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019q2Cfg V Pt) [hd2 : Fact (Eq (Module.finrank Real V) 2)] : Ne cfg.A₂ cfg.P

theorem Imo2019Q2.Imo2019q2Cfg.A₂_ne_B {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace Real V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019q2Cfg V Pt) [hd2 : Fact (Eq (Module.finrank Real V) 2)] : Ne cfg.A₂ cfg.B

theorem Imo2019Q2.Imo2019q2Cfg.A₂_ne_C {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace Real V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019q2Cfg V Pt) [hd2 : Fact (Eq (Module.finrank Real V) 2)] : Ne cfg.A₂ cfg.C

theorem Imo2019Q2.Imo2019q2Cfg.B₂_ne_B {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace Real V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019q2Cfg V Pt) [hd2 : Fact (Eq (Module.finrank Real V) 2)] : Ne cfg.B₂ cfg.B

theorem Imo2019Q2.Imo2019q2Cfg.B₂_ne_Q {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace Real V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019q2Cfg V Pt) [hd2 : Fact (Eq (Module.finrank Real V) 2)] : Ne cfg.B₂ cfg.Q

theorem Imo2019Q2.Imo2019q2Cfg.B₂_ne_A₂ {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace Real V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019q2Cfg V Pt) [hd2 : Fact (Eq (Module.finrank Real V) 2)] : Ne cfg.B₂ cfg.A₂

theorem Imo2019Q2.Imo2019q2Cfg.wbtw_B_Q_B₂ {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace Real V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019q2Cfg V Pt) [hd2 : Fact (Eq (Module.finrank Real V) 2)] : Wbtw Real cfg.B cfg.Q cfg.B₂

The first equality in the first angle chase in the solution

theorem Imo2019Q2.Imo2019q2Cfg.two_zsmul_oangle_QPA₂_eq_two_zsmul_oangle_BAA₂ {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace Real V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019q2Cfg V Pt) [hd2 : Fact (Eq (Module.finrank Real V) 2)] [Module.Oriented Real V (Fin 2)] : Eq (HSMul.hSMul 2 (EuclideanGeometry.oangle cfg.Q cfg.P cfg.A₂)) (HSMul.hSMul 2 (EuclideanGeometry.oangle cfg.B cfg.A cfg.A₂))

More obvious configuration properties

theorem Imo2019Q2.Imo2019q2Cfg.not_collinear_QPA₂ {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace Real V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019q2Cfg V Pt) [hd2 : Fact (Eq (Module.finrank Real V) 2)] : Not (Collinear Real (Insert.insert cfg.Q (Insert.insert cfg.P (Singleton.singleton cfg.A₂))))

theorem Imo2019Q2.Imo2019q2Cfg.Q₁_ne_A₂ {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace Real V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019q2Cfg V Pt) [hd2 : Fact (Eq (Module.finrank Real V) 2)] : Ne cfg.Q₁ cfg.A₂

theorem Imo2019Q2.Imo2019q2Cfg.affineIndependent_QPA₂ {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace Real V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019q2Cfg V Pt) [hd2 : Fact (Eq (Module.finrank Real V) 2)] : AffineIndependent Real (Matrix.vecCons cfg.Q (Matrix.vecCons cfg.P (Matrix.vecCons cfg.A₂ Matrix.vecEmpty)))

theorem Imo2019Q2.Imo2019q2Cfg.affineIndependent_PQB₂ {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace Real V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019q2Cfg V Pt) [hd2 : Fact (Eq (Module.finrank Real V) 2)] : AffineIndependent Real (Matrix.vecCons cfg.P (Matrix.vecCons cfg.Q (Matrix.vecCons cfg.B₂ Matrix.vecEmpty)))

def Imo2019Q2.Imo2019q2Cfg.triangleQPA₂ {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace Real V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019q2Cfg V Pt) [hd2 : Fact (Eq (Module.finrank Real V) 2)] : Affine.Triangle Real Pt

QPA₂ as a Triangle.

Equations

• Eq cfg.triangleQPA₂ { points := Matrix.vecCons cfg.Q (Matrix.vecCons cfg.P (Matrix.vecCons cfg.A₂ Matrix.vecEmpty)), independent := ⋯ }

def Imo2019Q2.Imo2019q2Cfg.trianglePQB₂ {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace Real V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019q2Cfg V Pt) [hd2 : Fact (Eq (Module.finrank Real V) 2)] : Affine.Triangle Real Pt

PQB₂ as a Triangle.

Equations

• Eq cfg.trianglePQB₂ { points := Matrix.vecCons cfg.P (Matrix.vecCons cfg.Q (Matrix.vecCons cfg.B₂ Matrix.vecEmpty)), independent := ⋯ }

theorem Imo2019Q2.Imo2019q2Cfg.symm_triangleQPA₂ {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace Real V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019q2Cfg V Pt) [hd2 : Fact (Eq (Module.finrank Real V) 2)] : Eq cfg.symm.triangleQPA₂ cfg.trianglePQB₂

def Imo2019Q2.Imo2019q2Cfg.ω {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace Real V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019q2Cfg V Pt) [hd2 : Fact (Eq (Module.finrank Real V) 2)] : EuclideanGeometry.Sphere Pt

ω is the circle containing Q, P and A₂, which will be shown also to contain B₂, P₁ and Q₁.

Equations

• Eq cfg.ω (Affine.Simplex.circumsphere cfg.triangleQPA₂)

theorem Imo2019Q2.Imo2019q2Cfg.P_mem_ω {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace Real V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019q2Cfg V Pt) [hd2 : Fact (Eq (Module.finrank Real V) 2)] : Membership.mem cfg.ω cfg.P

theorem Imo2019Q2.Imo2019q2Cfg.Q_mem_ω {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace Real V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019q2Cfg V Pt) [hd2 : Fact (Eq (Module.finrank Real V) 2)] : Membership.mem cfg.ω cfg.Q

The rest of the first angle chase in the solution

theorem Imo2019Q2.Imo2019q2Cfg.two_zsmul_oangle_QPA₂_eq_two_zsmul_oangle_QB₂A₂ {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace Real V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019q2Cfg V Pt) [hd2 : Fact (Eq (Module.finrank Real V) 2)] [Module.Oriented Real V (Fin 2)] : Eq (HSMul.hSMul 2 (EuclideanGeometry.oangle cfg.Q cfg.P cfg.A₂)) (HSMul.hSMul 2 (EuclideanGeometry.oangle cfg.Q cfg.B₂ cfg.A₂))

Conclusions from that first angle chase

theorem Imo2019Q2.Imo2019q2Cfg.cospherical_QPB₂A₂ {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace Real V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019q2Cfg V Pt) [hd2 : Fact (Eq (Module.finrank Real V) 2)] : EuclideanGeometry.Cospherical (Insert.insert cfg.Q (Insert.insert cfg.P (Insert.insert cfg.B₂ (Singleton.singleton cfg.A₂))))

theorem Imo2019Q2.Imo2019q2Cfg.symm_ω_eq_trianglePQB₂_circumsphere {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace Real V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019q2Cfg V Pt) [hd2 : Fact (Eq (Module.finrank Real V) 2)] : Eq cfg.symm.ω (Affine.Simplex.circumsphere cfg.trianglePQB₂)

theorem Imo2019Q2.Imo2019q2Cfg.symm_ω {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace Real V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019q2Cfg V Pt) [hd2 : Fact (Eq (Module.finrank Real V) 2)] : Eq cfg.symm.ω cfg.ω

The second angle chase in the solution

theorem Imo2019Q2.Imo2019q2Cfg.two_zsmul_oangle_CA₂A₁_eq_two_zsmul_oangle_CBA {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace Real V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019q2Cfg V Pt) [hd2 : Fact (Eq (Module.finrank Real V) 2)] [Module.Oriented Real V (Fin 2)] : Eq (HSMul.hSMul 2 (EuclideanGeometry.oangle cfg.C cfg.A₂ cfg.A₁)) (HSMul.hSMul 2 (EuclideanGeometry.oangle cfg.C cfg.B cfg.A))

theorem Imo2019Q2.Imo2019q2Cfg.two_zsmul_oangle_CA₂A₁_eq_two_zsmul_oangle_CQ₁A₁ {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace Real V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019q2Cfg V Pt) [hd2 : Fact (Eq (Module.finrank Real V) 2)] [Module.Oriented Real V (Fin 2)] : Eq (HSMul.hSMul 2 (EuclideanGeometry.oangle cfg.C cfg.A₂ cfg.A₁)) (HSMul.hSMul 2 (EuclideanGeometry.oangle cfg.C cfg.Q₁ cfg.A₁))

Conclusions from that second angle chase

theorem Imo2019Q2.Imo2019q2Cfg.not_collinear_CA₂A₁ {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace Real V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019q2Cfg V Pt) [hd2 : Fact (Eq (Module.finrank Real V) 2)] : Not (Collinear Real (Insert.insert cfg.C (Insert.insert cfg.A₂ (Singleton.singleton cfg.A₁))))

theorem Imo2019Q2.Imo2019q2Cfg.cospherical_A₁Q₁CA₂ {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace Real V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019q2Cfg V Pt) [hd2 : Fact (Eq (Module.finrank Real V) 2)] : EuclideanGeometry.Cospherical (Insert.insert cfg.A₁ (Insert.insert cfg.Q₁ (Insert.insert cfg.C (Singleton.singleton cfg.A₂))))

The third angle chase in the solution

theorem Imo2019Q2.Imo2019q2Cfg.two_zsmul_oangle_QQ₁A₂_eq_two_zsmul_oangle_QPA₂ {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace Real V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019q2Cfg V Pt) [hd2 : Fact (Eq (Module.finrank Real V) 2)] [Module.Oriented Real V (Fin 2)] : Eq (HSMul.hSMul 2 (EuclideanGeometry.oangle cfg.Q cfg.Q₁ cfg.A₂)) (HSMul.hSMul 2 (EuclideanGeometry.oangle cfg.Q cfg.P cfg.A₂))

Conclusions from that third angle chase

theorem Imo2019Q2.Imo2019q2Cfg.Q₁_mem_ω {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace Real V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019q2Cfg V Pt) [hd2 : Fact (Eq (Module.finrank Real V) 2)] : Membership.mem cfg.ω cfg.Q₁

theorem Imo2019Q2.Imo2019q2Cfg.P₁_mem_ω {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace Real V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019q2Cfg V Pt) [hd2 : Fact (Eq (Module.finrank Real V) 2)] : Membership.mem cfg.ω cfg.P₁

theorem Imo2019Q2.Imo2019q2Cfg.result {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace Real V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019q2Cfg V Pt) [hd2 : Fact (Eq (Module.finrank Real V) 2)] : EuclideanGeometry.Concyclic (Insert.insert cfg.P (Insert.insert cfg.Q (Insert.insert cfg.P₁ (Singleton.singleton cfg.Q₁))))

theorem imo2019_q2 (V : Type u_1) (Pt : Type u_2) [NormedAddCommGroup V] [InnerProductSpace Real V] [MetricSpace Pt] [NormedAddTorsor V Pt] [Fact (Eq (Module.finrank Real V) 2)] (A B C A₁ B₁ P Q P₁ Q₁ : Pt) (affine_independent_ABC : AffineIndependent Real (Matrix.vecCons A (Matrix.vecCons B (Matrix.vecCons C Matrix.vecEmpty)))) (wbtw_B_A₁_C : Wbtw Real B A₁ C) (wbtw_A_B₁_C : Wbtw Real A B₁ C) (wbtw_A_P_A₁ : Wbtw Real A P A₁) (wbtw_B_Q_B₁ : Wbtw Real B Q B₁) (PQ_parallel_AB : (affineSpan Real (Insert.insert P (Singleton.singleton Q))).Parallel (affineSpan Real (Insert.insert A (Singleton.singleton B)))) (P_ne_Q : Ne P Q) (sbtw_P_B₁_P₁ : Sbtw Real P B₁ P₁) (angle_PP₁C_eq_angle_BAC : Eq (EuclideanGeometry.angle P P₁ C) (EuclideanGeometry.angle B A C)) (C_ne_P₁ : Ne C P₁) (sbtw_Q_A₁_Q₁ : Sbtw Real Q A₁ Q₁) (angle_CQ₁Q_eq_angle_CBA : Eq (EuclideanGeometry.angle C Q₁ Q) (EuclideanGeometry.angle C B A)) (C_ne_Q₁ : Ne C Q₁) : EuclideanGeometry.Concyclic (Insert.insert P (Insert.insert Q (Insert.insert P₁ (Singleton.singleton Q₁))))