Product of the segments of chords

Proved

FamousTheorems.intersecting_chords

by cm_beta · Sep 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

euclidean-geometrygeometrymathlib

The intersecting chords theorem.

If $a, b, c, d$ lie on a common sphere and the chords $ab$ and $cd$ both pass through a point $p$ , then

|ap|\cdot|bp| \;=\; |cp|\cdot|dp| .

The common value depends only on $p$ and the sphere, not on the chord chosen: it is $r^2 - d(O,p)^2$ where $O$ is the centre. That quantity is the power of the point $p$ , and this theorem is the statement that the power is well defined — which is why every chord through $p$ is split in the same proportion. The external version, with $p$ outside the circle, gives the tangent–secant relation, and the locus of points of equal power with respect to two circles is their radical axis.

Euclid proves it as III.35, with III.36 and III.37 for the external cases. Steiner's systematic use of the power of a point in the 1820s turned it from a proposition about circles into the organising idea of inversive geometry.

Formalization note. $\angle\,apb = \pi$ says $p$ lies strictly between $a$ and $b$ , i.e. $p$ is interior to the chord. The result is Mathlib's EuclideanGeometry.mul_dist_eq_mul_dist_of_cospherical_of_angle_eq_pi.

Preamble

import Mathlib

Formal statement

namespace FamousTheorems

open scoped EuclideanGeometry Real

theorem intersecting_chords
    {V : Type*} {P : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V]
    [MetricSpace P] [NormedAddTorsor V P]
    {a b c d p : P} (h : EuclideanGeometry.Cospherical ({a, b, c, d} : Set P))
    (hapb : ∠ a p b = π) (hcpd : ∠ c p d = π) :
    dist a p * dist b p = dist c p * dist d p := by sorry

end FamousTheorems

Source

One of Freek Wiedijk's "100 theorems"; formalized in Mathlib. Proof here reduces to the corresponding Mathlib result.

View graph