English
Let s be a sphere with radius r and center c, and let p lie on a line through two points a, b on s. If 0 ≤ r and dist(p,c) ≥ r, then the product dist(p,a) dist(p,b) equals the power s.power(p) of p with respect to the sphere.
Русский
Пусть s — сфера с радиусом r и центром c, и p лежит на прямой, проходящей через две точки a, b на s. Пусть 0 ≤ r и расстояние dist(p, c) не меньше r; тогда произведение dist(p,a) dist(p,b) равно мощности точки p относительно сферы.
LaTeX
$$$\forall s:\text{Sphere}(P),\; p,a,b\in P:\; hr\colon 0\le s.radius \land p\in \mathrm{line}(a,b) \land a\in s \land b\in s \land s.radius \le \operatorname{dist}(p,s.center)\Rightarrow \operatorname{dist}(p,a)\operatorname{dist}(p,b)=s.power(p)$$$
Lean4
/-- For a point outside or on the sphere, the product of distances to two intersection
points on a line through the point equals the power of the point. -/
theorem mul_dist_eq_power_of_radius_le_dist_center {s : Sphere P} {p a b : P} (hr : 0 ≤ s.radius)
(hp : p ∈ line[ℝ, a, b]) (ha : a ∈ s) (hb : b ∈ s) (hle : s.radius ≤ dist p s.center) :
dist p a * dist p b = s.power p := by
rw [mul_dist_eq_abs_power hp ha hb, abs_of_nonneg <| (power_nonneg_iff_radius_le_dist_center hr).mpr hle]
