IMO 2001 Q5

Let ABC be a triangle. Let AP bisect ∠BAC and let BQ bisect ∠ABC, with P on BC and Q on AC. If AB + BP = AQ + QB and ∠BAC = 60°, what are the angles of the triangle?

Solution

We follow the solution from https://web.evanchen.cc/exams/IMO-2001-notes.pdf.

Let x = ∠ABQ = ∠QBC; it must be in (0°, 60°). By angle chasing and the law of sines we derive

1 + sin 30° / sin (150° - 2x) = (sin x + sin 60°) / sin (120° - x)

Solving this equation gives x = 40°, yielding ∠ABC = 80° and ∠ACB = 40°.

structure Imo2001Q5.Setup {V : Type u_1} (X : Type u_2) [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace X] [NormedAddTorsor V X] : Type u_2

The problem's configuration.

• A : X
• B : X
• C : X
• P : X
• Q : X
• P_on_BC : Wbtw ℝ self.B self.P self.C
• AP_bisect_BAC : EuclideanGeometry.angle self.B self.A self.P = EuclideanGeometry.angle self.P self.A self.C
• Q_on_AC : Wbtw ℝ self.A self.Q self.C
• BQ_bisect_ABC : EuclideanGeometry.angle self.A self.B self.Q = EuclideanGeometry.angle self.Q self.B self.C
• dist_sum : dist self.A self.B + dist self.B self.P = dist self.A self.Q + dist self.Q self.B
• BAC_eq : EuclideanGeometry.angle self.B self.A self.C = Real.pi / 3

Nondegeneracy properties and values of angles

theorem Imo2001Q5.Setup.A_ne_B {V : Type u_1} {X : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace X] [NormedAddTorsor V X] (s : Setup X) : s.A ≠ s.B

theorem Imo2001Q5.Setup.A_ne_C {V : Type u_1} {X : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace X] [NormedAddTorsor V X] (s : Setup X) : s.A ≠ s.C

theorem Imo2001Q5.Setup.B_ne_C {V : Type u_1} {X : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace X] [NormedAddTorsor V X] (s : Setup X) : s.B ≠ s.C

theorem Imo2001Q5.Setup.not_collinear_BAC {V : Type u_1} {X : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace X] [NormedAddTorsor V X] (s : Setup X) : ¬Collinear ℝ {s.B, s.A, s.C}

theorem Imo2001Q5.Setup.BAP_eq {V : Type u_1} {X : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace X] [NormedAddTorsor V X] (s : Setup X) : EuclideanGeometry.angle s.B s.A s.P = Real.pi / 6

theorem Imo2001Q5.Setup.PAC_eq {V : Type u_1} {X : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace X] [NormedAddTorsor V X] (s : Setup X) : EuclideanGeometry.angle s.P s.A s.C = Real.pi / 6

theorem Imo2001Q5.Setup.P_ne_B {V : Type u_1} {X : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace X] [NormedAddTorsor V X] (s : Setup X) : s.P ≠ s.B

theorem Imo2001Q5.Setup.P_ne_C {V : Type u_1} {X : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace X] [NormedAddTorsor V X] (s : Setup X) : s.P ≠ s.C

theorem Imo2001Q5.Setup.sbtw_BPC {V : Type u_1} {X : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace X] [NormedAddTorsor V X] (s : Setup X) : Sbtw ℝ s.B s.P s.C

theorem Imo2001Q5.Setup.BPC_eq {V : Type u_1} {X : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace X] [NormedAddTorsor V X] (s : Setup X) : EuclideanGeometry.angle s.B s.P s.C = Real.pi

def Imo2001Q5.Setup.x {V : Type u_1} {X : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace X] [NormedAddTorsor V X] (s : Setup X) : ℝ

x = ∠ABQ = ∠QBC. This is the main angle in the solution and it suffices to show this is 2 * π / 9.

Equations

• s.x = EuclideanGeometry.angle s.A s.B s.Q

theorem Imo2001Q5.Setup.ABQ_eq {V : Type u_1} {X : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace X] [NormedAddTorsor V X] (s : Setup X) : EuclideanGeometry.angle s.A s.B s.Q = s.x

theorem Imo2001Q5.Setup.QBC_eq {V : Type u_1} {X : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace X] [NormedAddTorsor V X] (s : Setup X) : EuclideanGeometry.angle s.Q s.B s.C = s.x

theorem Imo2001Q5.Setup.ABC_eq {V : Type u_1} {X : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace X] [NormedAddTorsor V X] (s : Setup X) : EuclideanGeometry.angle s.A s.B s.C = 2 * s.x

theorem Imo2001Q5.Setup.x_pos {V : Type u_1} {X : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace X] [NormedAddTorsor V X] (s : Setup X) : 0 < s.x

theorem Imo2001Q5.Setup.Q_ne_A {V : Type u_1} {X : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace X] [NormedAddTorsor V X] (s : Setup X) : s.Q ≠ s.A

theorem Imo2001Q5.Setup.Q_ne_C {V : Type u_1} {X : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace X] [NormedAddTorsor V X] (s : Setup X) : s.Q ≠ s.C

theorem Imo2001Q5.Setup.sbtw_AQC {V : Type u_1} {X : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace X] [NormedAddTorsor V X] (s : Setup X) : Sbtw ℝ s.A s.Q s.C

theorem Imo2001Q5.Setup.AQC_eq {V : Type u_1} {X : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace X] [NormedAddTorsor V X] (s : Setup X) : EuclideanGeometry.angle s.A s.Q s.C = Real.pi

theorem Imo2001Q5.Setup.ACB_eq {V : Type u_1} {X : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace X] [NormedAddTorsor V X] (s : Setup X) : EuclideanGeometry.angle s.A s.C s.B = 2 * Real.pi / 3 - 2 * s.x

theorem Imo2001Q5.Setup.x_lt_pi_div_three {V : Type u_1} {X : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace X] [NormedAddTorsor V X] (s : Setup X) : s.x < Real.pi / 3

theorem Imo2001Q5.Setup.APB_eq {V : Type u_1} {X : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace X] [NormedAddTorsor V X] (s : Setup X) : EuclideanGeometry.angle s.A s.P s.B = 5 * Real.pi / 6 - 2 * s.x

theorem Imo2001Q5.Setup.AQB_eq {V : Type u_1} {X : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace X] [NormedAddTorsor V X] (s : Setup X) : EuclideanGeometry.angle s.A s.Q s.B = 2 * Real.pi / 3 - s.x

def Imo2001Q5.Setup.bx : Lean.ParserDescr

A macro for applying the bounds on x, x_pos and x_lt_pi_div_three.

Equations

• Imo2001Q5.Setup.bx = Lean.ParserDescr.node `Imo2001Q5.Setup.bx 1024 (Lean.ParserDescr.nonReservedSymbol "bx" false)

Trigonometric reduction using the law of sines

theorem Imo2001Q5.Setup.BP_by_AB {V : Type u_1} {X : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace X] [NormedAddTorsor V X] (s : Setup X) : dist s.B s.P = Real.sin (Real.pi / 6) / Real.sin (5 * Real.pi / 6 - 2 * s.x) * dist s.A s.B

dist B P in terms of dist A B.

theorem Imo2001Q5.Setup.AQ_by_AB {V : Type u_1} {X : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace X] [NormedAddTorsor V X] (s : Setup X) : dist s.A s.Q = Real.sin s.x / Real.sin (2 * Real.pi / 3 - s.x) * dist s.A s.B

dist A Q in terms of dist A B.

theorem Imo2001Q5.Setup.QB_by_AB {V : Type u_1} {X : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace X] [NormedAddTorsor V X] (s : Setup X) : dist s.Q s.B = Real.sin (Real.pi / 3) / Real.sin (2 * Real.pi / 3 - s.x) * dist s.A s.B

dist Q B in terms of dist A B.

theorem Imo2001Q5.Setup.key_x_equation {V : Type u_1} {X : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace X] [NormedAddTorsor V X] (s : Setup X) : 1 + Real.sin (Real.pi / 6) / Real.sin (5 * Real.pi / 6 - 2 * s.x) = (Real.sin s.x + Real.sin (Real.pi / 3)) / Real.sin (2 * Real.pi / 3 - s.x)

The key trigonometric equation for x.

Solving the trigonometric equation

theorem Imo2001Q5.Setup.x_eq {V : Type u_1} {X : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace X] [NormedAddTorsor V X] (s : Setup X) : s.x = 2 * Real.pi / 9

theorem Imo2001Q5.result {V : Type u_1} {X : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace X] [NormedAddTorsor V X] (s : Setup X) : EuclideanGeometry.angle s.A s.B s.C = 4 * Real.pi / 9 ∧ EuclideanGeometry.angle s.A s.C s.B = 2 * Real.pi / 9