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 : Pt
- B : Pt
- C : Pt
- A₁ : Pt
- B₁ : Pt
- P : Pt
- Q : Pt
- P₁ : Pt
- Q₁ : Pt
- affineIndependent_ABC : AffineIndependent ℝ ![s.A, s.B, s.C]
- PQ_parallel_AB : AffineSubspace.Parallel (affineSpan ℝ {s.P, s.Q}) (affineSpan ℝ {s.A, s.B})
- P_ne_Q : s.P ≠ s.Q
- angle_PP₁C_eq_angle_BAC : EuclideanGeometry.angle s.P s.P₁ s.C = EuclideanGeometry.angle s.B s.A s.C
- C_ne_P₁ : s.C ≠ s.P₁
- angle_CQ₁Q_eq_angle_CBA : EuclideanGeometry.angle s.C s.Q₁ s.Q = EuclideanGeometry.angle s.C s.B s.A
- C_ne_Q₁ : s.C ≠ s.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
A default choice of orientation, for lemmas that need to pick one.
Instances For
The configuration has symmetry, allowing results proved for one point to be applied for another (where the informal solution says "similarly").
Instances For
Configuration properties that are obvious from the diagram, and construction of the #
ABC
as a Triangle
.
Instances For
A₂
is the second point of intersection of the ray AA₁
with the circumcircle of ABC
.
Instances For
B₂
is the second point of intersection of the ray BB₁
with the circumcircle of ABC
.
Instances For
Relate the orientations of different angles in the configuration #
More obvious configuration properties #
The first equality in the first angle chase in the solution #
More obvious configuration properties #
QPA₂
as a Triangle
.
Instances For
PQB₂
as a Triangle
.
Instances For
ω
is the circle containing Q
, P
and A₂
, which will be shown also to contain B₂
,
P₁
and Q₁
.