English
For any line through a point p intersecting a sphere at two points a,b, the product dist(p,a)dist(p,b) equals the absolute value of the sphere's power at p.
Русский
Для любой прямой через точку p, пересекающей сферу в две точки a,b, произведение dist(p,a)dist(p,b) равно модулю мощности сферы в p.
LaTeX
$$dist(p,a) \cdot dist(p,b) = |s.power(p)|$$
Lean4
/-- For any point, the product of distances to two intersection
points on a line through the point equals the absolute value of the power of the point. -/
theorem mul_dist_eq_abs_power {s : Sphere P} {p a b : P} (hp : p ∈ line[ℝ, a, b]) (ha : a ∈ s) (hb : b ∈ s) :
dist p a * dist p b = |s.power p| :=
by
have hq : dist a s.center = dist b s.center := by rw [mem_sphere.mp ha, mem_sphere.mp hb]
rw [dist_comm p a, dist_comm p b, mul_dist_eq_abs_sub_sq_dist hp hq, mem_sphere.mp hb, power, abs_sub_comm]
