dist_sq_mul_dist_add_dist_sq_mul_dist

English

Relates the lengths in a triangle with a cevian: sum of two squared distances along sides equals a product expression involving midpoint.

Русский

Связь длин сторон треугольника и отрезка cevian через формулу середины.

LaTeX

$$$\operatorname{dist}(a,b)^2 + \operatorname{dist}(a,c)^2 = 2\left( \operatorname{dist}(a,\text{midpoint}(b,c))^2 + \left(\frac{\operatorname{dist}(b,c)}{2}\right)^2 \right)$$$

Lean4

/-- **Stewart's Theorem**. -/
theorem dist_sq_mul_dist_add_dist_sq_mul_dist (a b c p : P) (h : ∠ b p c = π) :
    dist a b ^ 2 * dist c p + dist a c ^ 2 * dist b p = dist b c * (dist a p ^ 2 + dist b p * dist c p) :=
  by
  rw [pow_two, pow_two, law_cos a p b, law_cos a p c, eq_sub_of_add_eq (angle_add_angle_eq_pi_of_angle_eq_pi a h),
    Real.cos_pi_sub, dist_eq_add_dist_of_angle_eq_pi h]
  ring

Похожие утверждения