English
For four cospherical points a,b,c,d and suitable collinearity conditions, the classical Ptolemy relation holds: dist(a,b) dist(c,d) + dist(b,c) dist(d,a) = dist(a,c) dist(b,d).
Русский
Для четырех кососпутанных точек a,b,c,d при подходящих условиях на углах выполняется теорема Птолемея: |ab|·|cd| + |bc|·|da| = |ac|·|bd|.
LaTeX
$$$\\text{Cospherical}({a,b,c,d}) \\;\\land\\; \\angle a p c = \\pi \\land \\angle b p d = \\pi \\Rightarrow |ab|\\cdot|cd| + |bc|\\cdot |da| = |ac|\\cdot |bd|$$$
Lean4
/-- **Ptolemy’s Theorem**. -/
theorem mul_dist_add_mul_dist_eq_mul_dist_of_cospherical {a b c d p : P} (h : Cospherical ({ a, b, c, d } : Set P))
(hapc : ∠ a p c = π) (hbpd : ∠ b p d = π) : dist a b * dist c d + dist b c * dist d a = dist a c * dist b d :=
by
have h' : Cospherical ({ a, c, b, d } : Set P) := by rwa [Set.insert_comm c b { d }]
have hmul := mul_dist_eq_mul_dist_of_cospherical_of_angle_eq_pi h' hapc hbpd
have hbp := left_dist_ne_zero_of_angle_eq_pi hbpd
have h₁ : dist c d = dist c p / dist b p * dist a b :=
by
rw [dist_mul_of_eq_angle_of_dist_mul b p a c p d, dist_comm a b]
· rw [angle_eq_angle_of_angle_eq_pi_of_angle_eq_pi hbpd hapc, angle_comm]
all_goals simp [field, mul_comm, hmul]
have h₂ : dist d a = dist a p / dist b p * dist b c :=
by
rw [dist_mul_of_eq_angle_of_dist_mul c p b d p a, dist_comm c b]
· rwa [angle_comm, angle_eq_angle_of_angle_eq_pi_of_angle_eq_pi]; rwa [angle_comm]
all_goals simp [field, mul_comm, hmul]
have h₃ : dist d p = dist a p * dist c p / dist b p := by simp [field, hmul]
have h₄ : ∀ x y : ℝ, x * (y * x) = x * x * y := fun x y => by rw [mul_left_comm, mul_comm]
simp [field, h₁, h₂, dist_eq_add_dist_of_angle_eq_pi hbpd, h₃, dist_comm a b, h₄, ← sq,
dist_sq_mul_dist_add_dist_sq_mul_dist b, hapc]
