Theorem·T28
The Pythagorean theorem
If a triangle has a right angle at C, the squared length of the opposite side equals the sum of the squared lengths of the two sides meeting at C.
In words
For any three points A, B, C in the plane, if there is a right angle at C, then the squared distance from A to B equals the squared distance from A to C plus the squared distance from B to C.
Never needed: F10 · A03 · A04 · A05 · A07 (computed from the citation graph, not asserted).
Proof
- 1
- 2in terms of . Using associativity, commutativity, and the inverse/identity laws of T26: (the middle step inserts and removes ; the last rewrites using (iv) and (v) applied to T26). Likewise . So (D070).
- 3Expand the squared distance. By D072: Expanding via distributivity and the sign rules, and using commutativity ( ):
- 4Use the hypothesis. Negating (H) and using (v) applied to T26 (then commuting): ( is its own inverse since and inverses are unique, L28 (ii)). Regrouping the four negative cross terms from the previous step, via commutativity/associativity:
- 5Combine. Summing the two expansions and applying the previous step:
- 6Conclude. By D072 and D070, and (since , ). Reordering the four terms with commutativity/associativity:
∎
Remarks
The oldest and most famous theorem in geometry (Euclid's Elements, Book I, Proposition 47), proved here purely algebraically via the bilinearity of the dot product:
, which collapses to
exactly when
. Working with
instead of distance avoids constructing
or taking square roots: the theorem already holds over
. Example, the familiar 3-4-5 triangle:
,
,
; then
, and
. The converse (equal squared distances forces a right angle) and the extension to actual, square-rooted distances over the reals are not developed here.