IMO 2019 Q2 #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 : ℤ) • _ _ _.
We apply the following conventions for formalizing IMO geometry problems. A problem is assumed
to take place in the plane unless that is clearly not intended, so it is not required to prove
that the points are coplanar (whether or not that in fact follows from the other conditions).
Angles in problem statements are taken to be unoriented. A reference to an angle ∠XYZ is taken
to imply that X and Z are not equal to Y, since choices of junk values play no role in
informal mathematics, and those implications are included as hypotheses for the problem whether
or not they follow from the other hypotheses. Similar, a reference to XY as a line is taken to
imply that X does not equal Y and that is included as a hypothesis, and a reference to XY
being parallel to something is considered a reference to it as a line. However, such an implicit
hypothesis about two points being different is included only once for any given two points (even
if it follows from more than one reference to a line or an angle), if X ≠ Y is included then
Y ≠ X is not included separately, and such hypotheses are not included in the case where there
is also a reference in the problem to a triangle including those two points, or to strict
betweenness of three points including those two. If betweenness is stated, it is taken to be
strict betweenness. However, segments and sides are taken to include their endpoints (unless
this makes a problem false), although those degenerate cases might not necessarily have been
considered when the problem was formulated and contestants might not have been expected to deal
with them. A reference to a point being on a side or a segment is expressed directly with wbtw
rather than more literally with affine_segment.
@[nolint]
structure
imo2019_q2.imo2019q2_cfg
(V : Type u_1)
(Pt : Type u_2)
[normed_add_comm_group V]
[inner_product_space ℝ V]
[metric_space Pt]
[normed_add_torsor V Pt]
[hd2 : fact (fdim V = 2)] :
Type u_2
- A : Pt
- B : Pt
- C : Pt
- A₁ : Pt
- B₁ : Pt
- P : Pt
- Q : Pt
- P₁ : Pt
- Q₁ : Pt
- affine_independent_ABC : affine_independent ℝ ![self.A, self.B, self.C]
- wbtw_B_A₁_C : wbtw ℝ self.B self.A₁ self.C
- wbtw_A_B₁_C : wbtw ℝ self.A self.B₁ self.C
- wbtw_A_P_A₁ : wbtw ℝ self.A self.P self.A₁
- wbtw_B_Q_B₁ : wbtw ℝ self.B self.Q self.B₁
- PQ_parallel_AB : (affine_span ℝ {self.P, self.Q}).parallel (affine_span ℝ {self.A, self.B})
- P_ne_Q : self.P ≠ self.Q
- sbtw_P_B₁_P₁ : sbtw ℝ self.P self.B₁ self.P₁
- angle_PP₁C_eq_angle_BAC : euclidean_geometry.angle self.P self.P₁ self.C = euclidean_geometry.angle self.B self.A self.C
- C_ne_P₁ : self.C ≠ self.P₁
- sbtw_Q_A₁_Q₁ : sbtw ℝ self.Q self.A₁ self.Q₁
- angle_CQ₁Q_eq_angle_CBA : euclidean_geometry.angle self.C self.Q₁ self.Q = euclidean_geometry.angle self.C self.B self.A
- C_ne_Q₁ : self.C ≠ self.Q₁
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 imo2019_q2.imo2019q2_cfg
- imo2019_q2.imo2019q2_cfg.has_sizeof_inst
noncomputable
def
imo2019_q2.some_orientation
(V : Type u_1)
[normed_add_comm_group V]
[inner_product_space ℝ V]
[hd2 : fact (fdim V = 2)] :
module.oriented ℝ V (fin 2)
A default choice of orientation, for lemmas that need to pick one.
Equations
def
imo2019_q2.imo2019q2_cfg.symm
{V : Type u_1}
{Pt : Type u_2}
[normed_add_comm_group V]
[inner_product_space ℝ V]
[metric_space Pt]
[normed_add_torsor V Pt]
[hd2 : fact (fdim V = 2)]
(cfg : imo2019_q2.imo2019q2_cfg V Pt) :
The configuration has symmetry, allowing results proved for one point to be applied for another (where the informal solution says "similarly").
Equations
- cfg.symm = {A := cfg.B, B := cfg.A, C := cfg.C, A₁ := cfg.B₁, B₁ := cfg.A₁, P := cfg.Q, Q := cfg.P, P₁ := cfg.Q₁, Q₁ := cfg.P₁, affine_independent_ABC := _, wbtw_B_A₁_C := _, wbtw_A_B₁_C := _, wbtw_A_P_A₁ := _, wbtw_B_Q_B₁ := _, PQ_parallel_AB := _, P_ne_Q := _, sbtw_P_B₁_P₁ := _, angle_PP₁C_eq_angle_BAC := _, C_ne_P₁ := _, sbtw_Q_A₁_Q₁ := _, angle_CQ₁Q_eq_angle_CBA := _, C_ne_Q₁ := _}
Configuration properties that are obvious from the diagram, and construction of the #
points A₂ and B₂
theorem
imo2019_q2.imo2019q2_cfg.A_ne_B
{V : Type u_1}
{Pt : Type u_2}
[normed_add_comm_group V]
[inner_product_space ℝ V]
[metric_space Pt]
[normed_add_torsor V Pt]
[hd2 : fact (fdim V = 2)]
(cfg : imo2019_q2.imo2019q2_cfg V Pt) :
theorem
imo2019_q2.imo2019q2_cfg.A_ne_C
{V : Type u_1}
{Pt : Type u_2}
[normed_add_comm_group V]
[inner_product_space ℝ V]
[metric_space Pt]
[normed_add_torsor V Pt]
[hd2 : fact (fdim V = 2)]
(cfg : imo2019_q2.imo2019q2_cfg V Pt) :
theorem
imo2019_q2.imo2019q2_cfg.B_ne_C
{V : Type u_1}
{Pt : Type u_2}
[normed_add_comm_group V]
[inner_product_space ℝ V]
[metric_space Pt]
[normed_add_torsor V Pt]
[hd2 : fact (fdim V = 2)]
(cfg : imo2019_q2.imo2019q2_cfg V Pt) :
theorem
imo2019_q2.imo2019q2_cfg.not_collinear_ABC
{V : Type u_1}
{Pt : Type u_2}
[normed_add_comm_group V]
[inner_product_space ℝ V]
[metric_space Pt]
[normed_add_torsor V Pt]
[hd2 : fact (fdim V = 2)]
(cfg : imo2019_q2.imo2019q2_cfg V Pt) :
def
imo2019_q2.imo2019q2_cfg.triangle_ABC
{V : Type u_1}
{Pt : Type u_2}
[normed_add_comm_group V]
[inner_product_space ℝ V]
[metric_space Pt]
[normed_add_torsor V Pt]
[hd2 : fact (fdim V = 2)]
(cfg : imo2019_q2.imo2019q2_cfg V Pt) :
affine.triangle ℝ Pt
ABC as a triangle.
Equations
- cfg.triangle_ABC = {points := ![cfg.A, cfg.B, cfg.C], independent := _}
theorem
imo2019_q2.imo2019q2_cfg.A_mem_circumsphere
{V : Type u_1}
{Pt : Type u_2}
[normed_add_comm_group V]
[inner_product_space ℝ V]
[metric_space Pt]
[normed_add_torsor V Pt]
[hd2 : fact (fdim V = 2)]
(cfg : imo2019_q2.imo2019q2_cfg V Pt) :
cfg.A ∈ affine.simplex.circumsphere cfg.triangle_ABC
theorem
imo2019_q2.imo2019q2_cfg.B_mem_circumsphere
{V : Type u_1}
{Pt : Type u_2}
[normed_add_comm_group V]
[inner_product_space ℝ V]
[metric_space Pt]
[normed_add_torsor V Pt]
[hd2 : fact (fdim V = 2)]
(cfg : imo2019_q2.imo2019q2_cfg V Pt) :
cfg.B ∈ affine.simplex.circumsphere cfg.triangle_ABC
theorem
imo2019_q2.imo2019q2_cfg.C_mem_circumsphere
{V : Type u_1}
{Pt : Type u_2}
[normed_add_comm_group V]
[inner_product_space ℝ V]
[metric_space Pt]
[normed_add_torsor V Pt]
[hd2 : fact (fdim V = 2)]
(cfg : imo2019_q2.imo2019q2_cfg V Pt) :
cfg.C ∈ affine.simplex.circumsphere cfg.triangle_ABC
theorem
imo2019_q2.imo2019q2_cfg.symm_triangle_ABC
{V : Type u_1}
{Pt : Type u_2}
[normed_add_comm_group V]
[inner_product_space ℝ V]
[metric_space Pt]
[normed_add_torsor V Pt]
[hd2 : fact (fdim V = 2)]
(cfg : imo2019_q2.imo2019q2_cfg V Pt) :
cfg.symm.triangle_ABC = affine.simplex.reindex cfg.triangle_ABC (equiv.swap 0 1)
theorem
imo2019_q2.imo2019q2_cfg.symm_triangle_ABC_circumsphere
{V : Type u_1}
{Pt : Type u_2}
[normed_add_comm_group V]
[inner_product_space ℝ V]
[metric_space Pt]
[normed_add_torsor V Pt]
[hd2 : fact (fdim V = 2)]
(cfg : imo2019_q2.imo2019q2_cfg V Pt) :
noncomputable
def
imo2019_q2.imo2019q2_cfg.A₂
{V : Type u_1}
{Pt : Type u_2}
[normed_add_comm_group V]
[inner_product_space ℝ V]
[metric_space Pt]
[normed_add_torsor V Pt]
[hd2 : fact (fdim V = 2)]
(cfg : imo2019_q2.imo2019q2_cfg V Pt) :
Pt
A₂ is the second point of intersection of the ray AA₁ with the circumcircle of ABC.
Equations
- cfg.A₂ = (affine.simplex.circumsphere cfg.triangle_ABC).second_inter cfg.A (cfg.A₁ -ᵥ cfg.A)
noncomputable
def
imo2019_q2.imo2019q2_cfg.B₂
{V : Type u_1}
{Pt : Type u_2}
[normed_add_comm_group V]
[inner_product_space ℝ V]
[metric_space Pt]
[normed_add_torsor V Pt]
[hd2 : fact (fdim V = 2)]
(cfg : imo2019_q2.imo2019q2_cfg V Pt) :
Pt
B₂ is the second point of intersection of the ray BB₁ with the circumcircle of ABC.
Equations
- cfg.B₂ = (affine.simplex.circumsphere cfg.triangle_ABC).second_inter cfg.B (cfg.B₁ -ᵥ cfg.B)
theorem
imo2019_q2.imo2019q2_cfg.A₂_mem_circumsphere
{V : Type u_1}
{Pt : Type u_2}
[normed_add_comm_group V]
[inner_product_space ℝ V]
[metric_space Pt]
[normed_add_torsor V Pt]
[hd2 : fact (fdim V = 2)]
(cfg : imo2019_q2.imo2019q2_cfg V Pt) :
cfg.A₂ ∈ affine.simplex.circumsphere cfg.triangle_ABC
theorem
imo2019_q2.imo2019q2_cfg.B₂_mem_circumsphere
{V : Type u_1}
{Pt : Type u_2}
[normed_add_comm_group V]
[inner_product_space ℝ V]
[metric_space Pt]
[normed_add_torsor V Pt]
[hd2 : fact (fdim V = 2)]
(cfg : imo2019_q2.imo2019q2_cfg V Pt) :
cfg.B₂ ∈ affine.simplex.circumsphere cfg.triangle_ABC
theorem
imo2019_q2.imo2019q2_cfg.symm_A₂
{V : Type u_1}
{Pt : Type u_2}
[normed_add_comm_group V]
[inner_product_space ℝ V]
[metric_space Pt]
[normed_add_torsor V Pt]
[hd2 : fact (fdim V = 2)]
(cfg : imo2019_q2.imo2019q2_cfg V Pt) :
theorem
imo2019_q2.imo2019q2_cfg.QP_parallel_BA
{V : Type u_1}
{Pt : Type u_2}
[normed_add_comm_group V]
[inner_product_space ℝ V]
[metric_space Pt]
[normed_add_torsor V Pt]
[hd2 : fact (fdim V = 2)]
(cfg : imo2019_q2.imo2019q2_cfg V Pt) :
(affine_span ℝ {cfg.Q, cfg.P}).parallel (affine_span ℝ {cfg.B, cfg.A})
theorem
imo2019_q2.imo2019q2_cfg.A_ne_A₁
{V : Type u_1}
{Pt : Type u_2}
[normed_add_comm_group V]
[inner_product_space ℝ V]
[metric_space Pt]
[normed_add_torsor V Pt]
[hd2 : fact (fdim V = 2)]
(cfg : imo2019_q2.imo2019q2_cfg V Pt) :
theorem
imo2019_q2.imo2019q2_cfg.collinear_PAA₁A₂
{V : Type u_1}
{Pt : Type u_2}
[normed_add_comm_group V]
[inner_product_space ℝ V]
[metric_space Pt]
[normed_add_torsor V Pt]
[hd2 : fact (fdim V = 2)]
(cfg : imo2019_q2.imo2019q2_cfg V Pt) :
theorem
imo2019_q2.imo2019q2_cfg.A₁_ne_C
{V : Type u_1}
{Pt : Type u_2}
[normed_add_comm_group V]
[inner_product_space ℝ V]
[metric_space Pt]
[normed_add_torsor V Pt]
[hd2 : fact (fdim V = 2)]
(cfg : imo2019_q2.imo2019q2_cfg V Pt) :
theorem
imo2019_q2.imo2019q2_cfg.B₁_ne_C
{V : Type u_1}
{Pt : Type u_2}
[normed_add_comm_group V]
[inner_product_space ℝ V]
[metric_space Pt]
[normed_add_torsor V Pt]
[hd2 : fact (fdim V = 2)]
(cfg : imo2019_q2.imo2019q2_cfg V Pt) :
theorem
imo2019_q2.imo2019q2_cfg.Q_not_mem_CB
{V : Type u_1}
{Pt : Type u_2}
[normed_add_comm_group V]
[inner_product_space ℝ V]
[metric_space Pt]
[normed_add_torsor V Pt]
[hd2 : fact (fdim V = 2)]
(cfg : imo2019_q2.imo2019q2_cfg V Pt) :
theorem
imo2019_q2.imo2019q2_cfg.Q_ne_B
{V : Type u_1}
{Pt : Type u_2}
[normed_add_comm_group V]
[inner_product_space ℝ V]
[metric_space Pt]
[normed_add_torsor V Pt]
[hd2 : fact (fdim V = 2)]
(cfg : imo2019_q2.imo2019q2_cfg V Pt) :
theorem
imo2019_q2.imo2019q2_cfg.s_opp_side_CB_Q_Q₁
{V : Type u_1}
{Pt : Type u_2}
[normed_add_comm_group V]
[inner_product_space ℝ V]
[metric_space Pt]
[normed_add_torsor V Pt]
[hd2 : fact (fdim V = 2)]
(cfg : imo2019_q2.imo2019q2_cfg V Pt) :
(affine_span ℝ {cfg.C, cfg.B}).s_opp_side cfg.Q cfg.Q₁
Relate the orientations of different angles in the configuration #
theorem
imo2019_q2.imo2019q2_cfg.oangle_CQ₁Q_sign_eq_oangle_CBA_sign
{V : Type u_1}
{Pt : Type u_2}
[normed_add_comm_group V]
[inner_product_space ℝ V]
[metric_space Pt]
[normed_add_torsor V Pt]
[hd2 : fact (fdim V = 2)]
(cfg : imo2019_q2.imo2019q2_cfg V Pt)
[module.oriented ℝ V (fin 2)] :
theorem
imo2019_q2.imo2019q2_cfg.oangle_CQ₁Q_eq_oangle_CBA
{V : Type u_1}
{Pt : Type u_2}
[normed_add_comm_group V]
[inner_product_space ℝ V]
[metric_space Pt]
[normed_add_torsor V Pt]
[hd2 : fact (fdim V = 2)]
(cfg : imo2019_q2.imo2019q2_cfg V Pt)
[module.oriented ℝ V (fin 2)] :
euclidean_geometry.oangle cfg.C cfg.Q₁ cfg.Q = euclidean_geometry.oangle cfg.C cfg.B cfg.A
More obvious configuration properties #
theorem
imo2019_q2.imo2019q2_cfg.A₁_ne_B
{V : Type u_1}
{Pt : Type u_2}
[normed_add_comm_group V]
[inner_product_space ℝ V]
[metric_space Pt]
[normed_add_torsor V Pt]
[hd2 : fact (fdim V = 2)]
(cfg : imo2019_q2.imo2019q2_cfg V Pt) :
theorem
imo2019_q2.imo2019q2_cfg.sbtw_B_A₁_C
{V : Type u_1}
{Pt : Type u_2}
[normed_add_comm_group V]
[inner_product_space ℝ V]
[metric_space Pt]
[normed_add_torsor V Pt]
[hd2 : fact (fdim V = 2)]
(cfg : imo2019_q2.imo2019q2_cfg V Pt) :
theorem
imo2019_q2.imo2019q2_cfg.sbtw_A_B₁_C
{V : Type u_1}
{Pt : Type u_2}
[normed_add_comm_group V]
[inner_product_space ℝ V]
[metric_space Pt]
[normed_add_torsor V Pt]
[hd2 : fact (fdim V = 2)]
(cfg : imo2019_q2.imo2019q2_cfg V Pt) :
theorem
imo2019_q2.imo2019q2_cfg.sbtw_A_A₁_A₂
{V : Type u_1}
{Pt : Type u_2}
[normed_add_comm_group V]
[inner_product_space ℝ V]
[metric_space Pt]
[normed_add_torsor V Pt]
[hd2 : fact (fdim V = 2)]
(cfg : imo2019_q2.imo2019q2_cfg V Pt) :
theorem
imo2019_q2.imo2019q2_cfg.sbtw_B_B₁_B₂
{V : Type u_1}
{Pt : Type u_2}
[normed_add_comm_group V]
[inner_product_space ℝ V]
[metric_space Pt]
[normed_add_torsor V Pt]
[hd2 : fact (fdim V = 2)]
(cfg : imo2019_q2.imo2019q2_cfg V Pt) :
theorem
imo2019_q2.imo2019q2_cfg.A₂_ne_A
{V : Type u_1}
{Pt : Type u_2}
[normed_add_comm_group V]
[inner_product_space ℝ V]
[metric_space Pt]
[normed_add_torsor V Pt]
[hd2 : fact (fdim V = 2)]
(cfg : imo2019_q2.imo2019q2_cfg V Pt) :
theorem
imo2019_q2.imo2019q2_cfg.A₂_ne_P
{V : Type u_1}
{Pt : Type u_2}
[normed_add_comm_group V]
[inner_product_space ℝ V]
[metric_space Pt]
[normed_add_torsor V Pt]
[hd2 : fact (fdim V = 2)]
(cfg : imo2019_q2.imo2019q2_cfg V Pt) :
theorem
imo2019_q2.imo2019q2_cfg.A₂_ne_B
{V : Type u_1}
{Pt : Type u_2}
[normed_add_comm_group V]
[inner_product_space ℝ V]
[metric_space Pt]
[normed_add_torsor V Pt]
[hd2 : fact (fdim V = 2)]
(cfg : imo2019_q2.imo2019q2_cfg V Pt) :
theorem
imo2019_q2.imo2019q2_cfg.A₂_ne_C
{V : Type u_1}
{Pt : Type u_2}
[normed_add_comm_group V]
[inner_product_space ℝ V]
[metric_space Pt]
[normed_add_torsor V Pt]
[hd2 : fact (fdim V = 2)]
(cfg : imo2019_q2.imo2019q2_cfg V Pt) :
theorem
imo2019_q2.imo2019q2_cfg.B₂_ne_B
{V : Type u_1}
{Pt : Type u_2}
[normed_add_comm_group V]
[inner_product_space ℝ V]
[metric_space Pt]
[normed_add_torsor V Pt]
[hd2 : fact (fdim V = 2)]
(cfg : imo2019_q2.imo2019q2_cfg V Pt) :
theorem
imo2019_q2.imo2019q2_cfg.B₂_ne_Q
{V : Type u_1}
{Pt : Type u_2}
[normed_add_comm_group V]
[inner_product_space ℝ V]
[metric_space Pt]
[normed_add_torsor V Pt]
[hd2 : fact (fdim V = 2)]
(cfg : imo2019_q2.imo2019q2_cfg V Pt) :
theorem
imo2019_q2.imo2019q2_cfg.B₂_ne_A₂
{V : Type u_1}
{Pt : Type u_2}
[normed_add_comm_group V]
[inner_product_space ℝ V]
[metric_space Pt]
[normed_add_torsor V Pt]
[hd2 : fact (fdim V = 2)]
(cfg : imo2019_q2.imo2019q2_cfg V Pt) :
theorem
imo2019_q2.imo2019q2_cfg.wbtw_B_Q_B₂
{V : Type u_1}
{Pt : Type u_2}
[normed_add_comm_group V]
[inner_product_space ℝ V]
[metric_space Pt]
[normed_add_torsor V Pt]
[hd2 : fact (fdim V = 2)]
(cfg : imo2019_q2.imo2019q2_cfg V Pt) :
The first equality in the first angle chase in the solution #
theorem
imo2019_q2.imo2019q2_cfg.two_zsmul_oangle_QPA₂_eq_two_zsmul_oangle_BAA₂
{V : Type u_1}
{Pt : Type u_2}
[normed_add_comm_group V]
[inner_product_space ℝ V]
[metric_space Pt]
[normed_add_torsor V Pt]
[hd2 : fact (fdim V = 2)]
(cfg : imo2019_q2.imo2019q2_cfg V Pt)
[module.oriented ℝ V (fin 2)] :
More obvious configuration properties #
theorem
imo2019_q2.imo2019q2_cfg.not_collinear_QPA₂
{V : Type u_1}
{Pt : Type u_2}
[normed_add_comm_group V]
[inner_product_space ℝ V]
[metric_space Pt]
[normed_add_torsor V Pt]
[hd2 : fact (fdim V = 2)]
(cfg : imo2019_q2.imo2019q2_cfg V Pt) :
theorem
imo2019_q2.imo2019q2_cfg.Q₁_ne_A₂
{V : Type u_1}
{Pt : Type u_2}
[normed_add_comm_group V]
[inner_product_space ℝ V]
[metric_space Pt]
[normed_add_torsor V Pt]
[hd2 : fact (fdim V = 2)]
(cfg : imo2019_q2.imo2019q2_cfg V Pt) :
theorem
imo2019_q2.imo2019q2_cfg.affine_independent_QPA₂
{V : Type u_1}
{Pt : Type u_2}
[normed_add_comm_group V]
[inner_product_space ℝ V]
[metric_space Pt]
[normed_add_torsor V Pt]
[hd2 : fact (fdim V = 2)]
(cfg : imo2019_q2.imo2019q2_cfg V Pt) :
theorem
imo2019_q2.imo2019q2_cfg.affine_independent_PQB₂
{V : Type u_1}
{Pt : Type u_2}
[normed_add_comm_group V]
[inner_product_space ℝ V]
[metric_space Pt]
[normed_add_torsor V Pt]
[hd2 : fact (fdim V = 2)]
(cfg : imo2019_q2.imo2019q2_cfg V Pt) :
noncomputable
def
imo2019_q2.imo2019q2_cfg.triangle_QPA₂
{V : Type u_1}
{Pt : Type u_2}
[normed_add_comm_group V]
[inner_product_space ℝ V]
[metric_space Pt]
[normed_add_torsor V Pt]
[hd2 : fact (fdim V = 2)]
(cfg : imo2019_q2.imo2019q2_cfg V Pt) :
affine.triangle ℝ Pt
QPA₂ as a triangle.
Equations
- cfg.triangle_QPA₂ = {points := ![cfg.Q, cfg.P, cfg.A₂], independent := _}
noncomputable
def
imo2019_q2.imo2019q2_cfg.triangle_PQB₂
{V : Type u_1}
{Pt : Type u_2}
[normed_add_comm_group V]
[inner_product_space ℝ V]
[metric_space Pt]
[normed_add_torsor V Pt]
[hd2 : fact (fdim V = 2)]
(cfg : imo2019_q2.imo2019q2_cfg V Pt) :
affine.triangle ℝ Pt
PQB₂ as a triangle.
Equations
- cfg.triangle_PQB₂ = {points := ![cfg.P, cfg.Q, cfg.B₂], independent := _}
theorem
imo2019_q2.imo2019q2_cfg.symm_triangle_QPA₂
{V : Type u_1}
{Pt : Type u_2}
[normed_add_comm_group V]
[inner_product_space ℝ V]
[metric_space Pt]
[normed_add_torsor V Pt]
[hd2 : fact (fdim V = 2)]
(cfg : imo2019_q2.imo2019q2_cfg V Pt) :
cfg.symm.triangle_QPA₂ = cfg.triangle_PQB₂
noncomputable
def
imo2019_q2.imo2019q2_cfg.ω
{V : Type u_1}
{Pt : Type u_2}
[normed_add_comm_group V]
[inner_product_space ℝ V]
[metric_space Pt]
[normed_add_torsor V Pt]
[hd2 : fact (fdim V = 2)]
(cfg : imo2019_q2.imo2019q2_cfg V Pt) :
ω is the circle containing Q, P and A₂, which will be shown also to contain B₂,
P₁ and Q₁.
Equations
- cfg.ω = affine.simplex.circumsphere cfg.triangle_QPA₂
theorem
imo2019_q2.imo2019q2_cfg.P_mem_ω
{V : Type u_1}
{Pt : Type u_2}
[normed_add_comm_group V]
[inner_product_space ℝ V]
[metric_space Pt]
[normed_add_torsor V Pt]
[hd2 : fact (fdim V = 2)]
(cfg : imo2019_q2.imo2019q2_cfg V Pt) :
theorem
imo2019_q2.imo2019q2_cfg.Q_mem_ω
{V : Type u_1}
{Pt : Type u_2}
[normed_add_comm_group V]
[inner_product_space ℝ V]
[metric_space Pt]
[normed_add_torsor V Pt]
[hd2 : fact (fdim V = 2)]
(cfg : imo2019_q2.imo2019q2_cfg V Pt) :
The rest of the first angle chase in the solution #
theorem
imo2019_q2.imo2019q2_cfg.two_zsmul_oangle_QPA₂_eq_two_zsmul_oangle_QB₂A₂
{V : Type u_1}
{Pt : Type u_2}
[normed_add_comm_group V]
[inner_product_space ℝ V]
[metric_space Pt]
[normed_add_torsor V Pt]
[hd2 : fact (fdim V = 2)]
(cfg : imo2019_q2.imo2019q2_cfg V Pt)
[module.oriented ℝ V (fin 2)] :
Conclusions from that first angle chase #
theorem
imo2019_q2.imo2019q2_cfg.cospherical_QPB₂A₂
{V : Type u_1}
{Pt : Type u_2}
[normed_add_comm_group V]
[inner_product_space ℝ V]
[metric_space Pt]
[normed_add_torsor V Pt]
[hd2 : fact (fdim V = 2)]
(cfg : imo2019_q2.imo2019q2_cfg V Pt) :
euclidean_geometry.cospherical {cfg.Q, cfg.P, cfg.B₂, cfg.A₂}
theorem
imo2019_q2.imo2019q2_cfg.symm_ω_eq_triangle_PQB₂_circumsphere
{V : Type u_1}
{Pt : Type u_2}
[normed_add_comm_group V]
[inner_product_space ℝ V]
[metric_space Pt]
[normed_add_torsor V Pt]
[hd2 : fact (fdim V = 2)]
(cfg : imo2019_q2.imo2019q2_cfg V Pt) :
cfg.symm.ω = affine.simplex.circumsphere cfg.triangle_PQB₂
theorem
imo2019_q2.imo2019q2_cfg.symm_ω
{V : Type u_1}
{Pt : Type u_2}
[normed_add_comm_group V]
[inner_product_space ℝ V]
[metric_space Pt]
[normed_add_torsor V Pt]
[hd2 : fact (fdim V = 2)]
(cfg : imo2019_q2.imo2019q2_cfg V Pt) :
The second angle chase in the solution #
theorem
imo2019_q2.imo2019q2_cfg.two_zsmul_oangle_CA₂A₁_eq_two_zsmul_oangle_CBA
{V : Type u_1}
{Pt : Type u_2}
[normed_add_comm_group V]
[inner_product_space ℝ V]
[metric_space Pt]
[normed_add_torsor V Pt]
[hd2 : fact (fdim V = 2)]
(cfg : imo2019_q2.imo2019q2_cfg V Pt)
[module.oriented ℝ V (fin 2)] :
theorem
imo2019_q2.imo2019q2_cfg.two_zsmul_oangle_CA₂A₁_eq_two_zsmul_oangle_CQ₁A₁
{V : Type u_1}
{Pt : Type u_2}
[normed_add_comm_group V]
[inner_product_space ℝ V]
[metric_space Pt]
[normed_add_torsor V Pt]
[hd2 : fact (fdim V = 2)]
(cfg : imo2019_q2.imo2019q2_cfg V Pt)
[module.oriented ℝ V (fin 2)] :
Conclusions from that second angle chase #
theorem
imo2019_q2.imo2019q2_cfg.not_collinear_CA₂A₁
{V : Type u_1}
{Pt : Type u_2}
[normed_add_comm_group V]
[inner_product_space ℝ V]
[metric_space Pt]
[normed_add_torsor V Pt]
[hd2 : fact (fdim V = 2)]
(cfg : imo2019_q2.imo2019q2_cfg V Pt) :
theorem
imo2019_q2.imo2019q2_cfg.cospherical_A₁Q₁CA₂
{V : Type u_1}
{Pt : Type u_2}
[normed_add_comm_group V]
[inner_product_space ℝ V]
[metric_space Pt]
[normed_add_torsor V Pt]
[hd2 : fact (fdim V = 2)]
(cfg : imo2019_q2.imo2019q2_cfg V Pt) :
euclidean_geometry.cospherical {cfg.A₁, cfg.Q₁, cfg.C, cfg.A₂}
The third angle chase in the solution #
theorem
imo2019_q2.imo2019q2_cfg.two_zsmul_oangle_QQ₁A₂_eq_two_zsmul_oangle_QPA₂
{V : Type u_1}
{Pt : Type u_2}
[normed_add_comm_group V]
[inner_product_space ℝ V]
[metric_space Pt]
[normed_add_torsor V Pt]
[hd2 : fact (fdim V = 2)]
(cfg : imo2019_q2.imo2019q2_cfg V Pt)
[module.oriented ℝ V (fin 2)] :
Conclusions from that third angle chase #
theorem
imo2019_q2.imo2019q2_cfg.Q₁_mem_ω
{V : Type u_1}
{Pt : Type u_2}
[normed_add_comm_group V]
[inner_product_space ℝ V]
[metric_space Pt]
[normed_add_torsor V Pt]
[hd2 : fact (fdim V = 2)]
(cfg : imo2019_q2.imo2019q2_cfg V Pt) :
theorem
imo2019_q2.imo2019q2_cfg.P₁_mem_ω
{V : Type u_1}
{Pt : Type u_2}
[normed_add_comm_group V]
[inner_product_space ℝ V]
[metric_space Pt]
[normed_add_torsor V Pt]
[hd2 : fact (fdim V = 2)]
(cfg : imo2019_q2.imo2019q2_cfg V Pt) :
theorem
imo2019_q2.imo2019q2_cfg.result
{V : Type u_1}
{Pt : Type u_2}
[normed_add_comm_group V]
[inner_product_space ℝ V]
[metric_space Pt]
[normed_add_torsor V Pt]
[hd2 : fact (fdim V = 2)]
(cfg : imo2019_q2.imo2019q2_cfg V Pt) :
euclidean_geometry.concyclic {cfg.P, cfg.Q, cfg.P₁, cfg.Q₁}
theorem
imo2019_q2
(V : Type u_1)
(Pt : Type u_2)
[normed_add_comm_group V]
[inner_product_space ℝ V]
[metric_space Pt]
[normed_add_torsor V Pt]
[hd2 : fact (fdim V = 2)]
(A B C A₁ B₁ P Q P₁ Q₁ : Pt)
(affine_independent_ABC : affine_independent ℝ ![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 : (affine_span ℝ {P, Q}).parallel (affine_span ℝ {A, B}))
(P_ne_Q : P ≠ Q)
(sbtw_P_B₁_P₁ : sbtw ℝ P B₁ P₁)
(angle_PP₁C_eq_angle_BAC : euclidean_geometry.angle P P₁ C = euclidean_geometry.angle B A C)
(C_ne_P₁ : C ≠ P₁)
(sbtw_Q_A₁_Q₁ : sbtw ℝ Q A₁ Q₁)
(angle_CQ₁Q_eq_angle_CBA : euclidean_geometry.angle C Q₁ Q = euclidean_geometry.angle C B A)
(C_ne_Q₁ : C ≠ Q₁) :
euclidean_geometry.concyclic {P, Q, P₁, Q₁}