English
A variant of the sine rule equates sin(angle p1 p2 p3)/dist(p3 p1) to sin(angle p3 p1 p2)/dist(p1 p2).
Русский
Вариант закона синусов, связывающий синус угла и расстояния между вершинами.
LaTeX
$$$\dfrac{\sin(\angle p_1 p_2 p_3)}{\operatorname{dist}(p_3,p_1)} = \dfrac{\sin(\angle p_2 p_3 p_1)}{\operatorname{dist}(p_1,p_2)}$$$
Lean4
theorem dist_mul_of_eq_angle_of_dist_mul (a b c a' b' c' : P) (r : ℝ) (h : ∠ a' b' c' = ∠ a b c)
(hab : dist a' b' = r * dist a b) (hcb : dist c' b' = r * dist c b) : dist a' c' = r * dist a c :=
by
have h' : dist a' c' ^ 2 = (r * dist a c) ^ 2 :=
calc
dist a' c' ^ 2 = dist a' b' ^ 2 + dist c' b' ^ 2 - 2 * dist a' b' * dist c' b' * Real.cos (∠ a' b' c') := by
simp [pow_two, law_cos a' b' c']
_ = r ^ 2 * (dist a b ^ 2 + dist c b ^ 2 - 2 * dist a b * dist c b * Real.cos (∠ a b c)) := by rw [h, hab, hcb];
ring
_ = (r * dist a c) ^ 2 := by simp [pow_two, ← law_cos a b c]; ring
by_cases hab₁ : a = b
· have hab'₁ : a' = b' := by rw [← dist_eq_zero, hab, dist_eq_zero.mpr hab₁, mul_zero r]
rw [hab₁, hab'₁, dist_comm b' c', dist_comm b c, hcb]
· have h1 : 0 ≤ r * dist a b := by rw [← hab]; exact dist_nonneg
have h2 : 0 ≤ r := nonneg_of_mul_nonneg_left h1 (dist_pos.mpr hab₁)
exact (sq_eq_sq₀ dist_nonneg (mul_nonneg h2 dist_nonneg)).mp h'
