Documentation

Archive.Imo.Imo2019Q2

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 : ℤ) • ∡ _ _ _.

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.

Instances For
    theorem Imo2019Q2.Imo2019q2Cfg.wbtw_B_A₁_C {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace V] [MetricSpace Pt] [NormedAddTorsor V Pt] (self : Imo2019Q2.Imo2019q2Cfg V Pt) :
    Wbtw self.B self.A₁ self.C
    theorem Imo2019Q2.Imo2019q2Cfg.wbtw_A_B₁_C {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace V] [MetricSpace Pt] [NormedAddTorsor V Pt] (self : Imo2019Q2.Imo2019q2Cfg V Pt) :
    Wbtw self.A self.B₁ self.C
    theorem Imo2019Q2.Imo2019q2Cfg.wbtw_A_P_A₁ {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace V] [MetricSpace Pt] [NormedAddTorsor V Pt] (self : Imo2019Q2.Imo2019q2Cfg V Pt) :
    Wbtw self.A self.P self.A₁
    theorem Imo2019Q2.Imo2019q2Cfg.wbtw_B_Q_B₁ {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace V] [MetricSpace Pt] [NormedAddTorsor V Pt] (self : Imo2019Q2.Imo2019q2Cfg V Pt) :
    Wbtw self.B self.Q self.B₁
    theorem Imo2019Q2.Imo2019q2Cfg.PQ_parallel_AB {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace V] [MetricSpace Pt] [NormedAddTorsor V Pt] (self : Imo2019Q2.Imo2019q2Cfg V Pt) :
    (affineSpan {self.P, self.Q}).Parallel (affineSpan {self.A, self.B})
    theorem Imo2019Q2.Imo2019q2Cfg.sbtw_P_B₁_P₁ {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace V] [MetricSpace Pt] [NormedAddTorsor V Pt] (self : Imo2019Q2.Imo2019q2Cfg V Pt) :
    Sbtw self.P self.B₁ self.P₁
    theorem Imo2019Q2.Imo2019q2Cfg.C_ne_P₁ {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace V] [MetricSpace Pt] [NormedAddTorsor V Pt] (self : Imo2019Q2.Imo2019q2Cfg V Pt) :
    self.C self.P₁
    theorem Imo2019Q2.Imo2019q2Cfg.sbtw_Q_A₁_Q₁ {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace V] [MetricSpace Pt] [NormedAddTorsor V Pt] (self : Imo2019Q2.Imo2019q2Cfg V Pt) :
    Sbtw self.Q self.A₁ self.Q₁
    theorem Imo2019Q2.Imo2019q2Cfg.C_ne_Q₁ {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace V] [MetricSpace Pt] [NormedAddTorsor V Pt] (self : Imo2019Q2.Imo2019q2Cfg V Pt) :
    self.C self.Q₁

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

    Equations
    Instances For

      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.
      Instances For

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

        points A₂ and B₂

        ABC as a Triangle.

        Equations
        • cfg.triangleABC = { points := ![cfg.A, cfg.B, cfg.C], independent := }
        Instances For
          theorem Imo2019Q2.Imo2019q2Cfg.symm_triangleABC {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) :
          cfg.symm.triangleABC = Affine.Simplex.reindex cfg.triangleABC (Equiv.swap 0 1)

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

          Equations
          Instances For

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

            Equations
            Instances For
              theorem Imo2019Q2.Imo2019q2Cfg.symm_A₂ {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) :
              cfg.symm.A₂ = cfg.B₂
              theorem Imo2019Q2.Imo2019q2Cfg.QP_parallel_BA {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) :
              (affineSpan {cfg.Q, cfg.P}).Parallel (affineSpan {cfg.B, cfg.A})
              theorem Imo2019Q2.Imo2019q2Cfg.collinear_PAA₁A₂ {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) :
              Collinear {cfg.P, cfg.A, cfg.A₁, cfg.A₂}
              theorem Imo2019Q2.Imo2019q2Cfg.sOppSide_CB_Q_Q₁ {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) :
              (affineSpan {cfg.C, cfg.B}).SOppSide cfg.Q cfg.Q₁

              Relate the orientations of different angles in the configuration #

              More obvious configuration properties #

              theorem Imo2019Q2.Imo2019q2Cfg.A₁_ne_B {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) [hd2 : Fact (Module.finrank V = 2)] :
              cfg.A₁ cfg.B
              theorem Imo2019Q2.Imo2019q2Cfg.sbtw_B_A₁_C {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) [hd2 : Fact (Module.finrank V = 2)] :
              Sbtw cfg.B cfg.A₁ cfg.C
              theorem Imo2019Q2.Imo2019q2Cfg.sbtw_A_B₁_C {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) [hd2 : Fact (Module.finrank V = 2)] :
              Sbtw cfg.A cfg.B₁ cfg.C
              theorem Imo2019Q2.Imo2019q2Cfg.sbtw_A_A₁_A₂ {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) [hd2 : Fact (Module.finrank V = 2)] :
              Sbtw cfg.A cfg.A₁ cfg.A₂
              theorem Imo2019Q2.Imo2019q2Cfg.sbtw_B_B₁_B₂ {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) [hd2 : Fact (Module.finrank V = 2)] :
              Sbtw cfg.B cfg.B₁ cfg.B₂
              theorem Imo2019Q2.Imo2019q2Cfg.A₂_ne_A {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) [hd2 : Fact (Module.finrank V = 2)] :
              cfg.A₂ cfg.A
              theorem Imo2019Q2.Imo2019q2Cfg.A₂_ne_P {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) [hd2 : Fact (Module.finrank V = 2)] :
              cfg.A₂ cfg.P
              theorem Imo2019Q2.Imo2019q2Cfg.A₂_ne_B {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) [hd2 : Fact (Module.finrank V = 2)] :
              cfg.A₂ cfg.B
              theorem Imo2019Q2.Imo2019q2Cfg.A₂_ne_C {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) [hd2 : Fact (Module.finrank V = 2)] :
              cfg.A₂ cfg.C
              theorem Imo2019Q2.Imo2019q2Cfg.B₂_ne_B {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) [hd2 : Fact (Module.finrank V = 2)] :
              cfg.B₂ cfg.B
              theorem Imo2019Q2.Imo2019q2Cfg.B₂_ne_Q {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) [hd2 : Fact (Module.finrank V = 2)] :
              cfg.B₂ cfg.Q
              theorem Imo2019Q2.Imo2019q2Cfg.B₂_ne_A₂ {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) [hd2 : Fact (Module.finrank V = 2)] :
              cfg.B₂ cfg.A₂
              theorem Imo2019Q2.Imo2019q2Cfg.wbtw_B_Q_B₂ {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) [hd2 : Fact (Module.finrank V = 2)] :
              Wbtw cfg.B cfg.Q cfg.B₂

              The first equality in the first angle chase in the solution #

              More obvious configuration properties #

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

              QPA₂ as a Triangle.

              Equations
              • cfg.triangleQPA₂ = { points := ![cfg.Q, cfg.P, cfg.A₂], independent := }
              Instances For

                PQB₂ as a Triangle.

                Equations
                • cfg.trianglePQB₂ = { points := ![cfg.P, cfg.Q, cfg.B₂], independent := }
                Instances For
                  theorem Imo2019Q2.Imo2019q2Cfg.symm_triangleQPA₂ {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) [hd2 : Fact (Module.finrank V = 2)] :
                  cfg.symm.triangleQPA₂ = cfg.trianglePQB₂

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

                  Equations
                  Instances For

                    The rest of the first angle chase in the solution #

                    Conclusions from that first angle chase #

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

                    The second angle chase in the solution #

                    Conclusions from that second angle chase #

                    The third angle chase in the solution #

                    Conclusions from that third angle chase #

                    theorem Imo2019Q2.Imo2019q2Cfg.Q₁_mem_ω {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) [hd2 : Fact (Module.finrank V = 2)] :
                    cfg.Q₁ cfg
                    theorem Imo2019Q2.Imo2019q2Cfg.P₁_mem_ω {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) [hd2 : Fact (Module.finrank V = 2)] :
                    cfg.P₁ cfg
                    theorem Imo2019Q2.Imo2019q2Cfg.result {V : Type u_1} {Pt : Type u_2} [NormedAddCommGroup V] [InnerProductSpace V] [MetricSpace Pt] [NormedAddTorsor V Pt] (cfg : Imo2019Q2.Imo2019q2Cfg V Pt) [hd2 : Fact (Module.finrank V = 2)] :
                    EuclideanGeometry.Concyclic {cfg.P, cfg.Q, cfg.P₁, cfg.Q₁}
                    theorem imo2019_q2 (V : Type u_1) (Pt : Type u_2) [NormedAddCommGroup V] [InnerProductSpace V] [MetricSpace Pt] [NormedAddTorsor V Pt] [Fact (Module.finrank V = 2)] (A : Pt) (B : Pt) (C : Pt) (A₁ : Pt) (B₁ : Pt) (P : Pt) (Q : Pt) (P₁ : Pt) (Q₁ : Pt) (affine_independent_ABC : AffineIndependent ![A, B, C]) (wbtw_B_A₁_C : Wbtw B A₁ C) (wbtw_A_B₁_C : Wbtw A B₁ C) (wbtw_A_P_A₁ : Wbtw A P A₁) (wbtw_B_Q_B₁ : Wbtw B Q B₁) (PQ_parallel_AB : (affineSpan {P, Q}).Parallel (affineSpan {A, B})) (P_ne_Q : P Q) (sbtw_P_B₁_P₁ : Sbtw P B₁ P₁) (angle_PP₁C_eq_angle_BAC : EuclideanGeometry.angle P P₁ C = EuclideanGeometry.angle B A C) (C_ne_P₁ : C P₁) (sbtw_Q_A₁_Q₁ : Sbtw Q A₁ Q₁) (angle_CQ₁Q_eq_angle_CBA : EuclideanGeometry.angle C Q₁ Q = EuclideanGeometry.angle C B A) (C_ne_Q₁ : C Q₁) :
                    EuclideanGeometry.Concyclic {P, Q, P₁, Q₁}