Euclidean geometry and proof

Lens

MotivationH

Why prove what you can see?

A carpenter in Nairobi is building a door frame. She has cut the two long sides to the same length, and the two short sides to the same length, and joined them. Is the frame a true rectangle, with four right angles? She does not reach for a protractor. She measures the two diagonals with a tape. If they are equal, the frame is "square". Builders all over the world use this trick. But why does it work? Could a frame have equal diagonals and still be skewed?

Here is a second puzzle. A famous "proof" that every triangle is isosceles goes like this. Take any triangle $ABC$ . Let the bisector of the angle at $A$ meet the perpendicular bisector of $BC$ at a point $P$ , drawn inside the triangle. Drop perpendiculars from $P$ to $AB$ and $AC$ . A few pairs of congruent triangles later, the argument concludes that $AB = AC$ . Every step seems to follow from the picture — and the conclusion is plainly false, since a triangle with sides $3$ , $4$ , $5$ is not isosceles.

The error is not in any calculation. It is in the picture: when $AB \ne AC$ , the point $P$ is never actually inside the triangle (we will see where it really is). This is why mathematicians prove geometric facts from stated assumptions, not from how a diagram looks. Euclid of Alexandria organised geometry this way around 300 BCE, and his Elements became the model of proof for two thousand years. In this lesson we will build up the main theorems about triangles and circles from a few axioms, see exactly where each axiom is used, and find out what happens when one of them is dropped.

IntuitionH

The rules of the game

A proof in geometry is a chain of statements, each justified by an axiom, a definition or an earlier theorem. The diagram helps us think; it is never a reason.

Euclid began with five postulates. In modern words:

Any two points can be joined by a straight line segment.
A segment can be extended indefinitely.
A circle can be drawn with any centre and any radius.
All right angles are equal.
If a line crossing two other lines makes the interior angles on one side add up to less than two right angles, then the two lines, extended far enough, meet on that side.

The fifth, the parallel postulate, is longer and less obvious than the others. For two thousand years mathematicians tried to prove it from the first four. They all failed, and in the 19th century it became clear why: it cannot be proved from them. We will come back to this.

Euclid's own list had gaps. He sometimes used facts that he never stated, such as "a line that enters a triangle through one side must leave through another". In 1899 David Hilbert gave a complete list of axioms for plane geometry, which fills those gaps. We will not list all of Hilbert's axioms. Instead we take as known the basic facts about points, lines, betweenness, lengths and angle measure that you have used for years, together with three things we state explicitly:

Angles on a straight line add up to $180^\circ$ , and vertically opposite angles are equal.
The SAS axiom (below). Euclid "proved" it by picking one triangle up and laying it on the other. That is really an assumption about rigid motions (see rigid motions, congruence and similarity), so Hilbert made it an axiom.
The parallel postulate, in the form of Playfair's axiom.

DefinitionsH

Definitions

Definition— congruent triangles

Triangles $ABC$ and $A'B'C'$ are congruent, written $\triangle ABC \cong \triangle A'B'C'$ , if corresponding sides and corresponding angles are equal: $AB = A'B'$ , $BC = B'C'$ , $CA = C'A'$ , $\angle A = \angle A'$ , $\angle B = \angle B'$ and $\angle C = \angle C'$ . The order of the letters records which vertex corresponds to which.

Definition— the SAS axiom

If $AB = A'B'$ , $AC = A'C'$ and the included angles are equal, $\angle BAC = \angle B'A'C'$ , then $\triangle ABC \cong \triangle A'B'C'$ .

From SAS one can prove two more congruence criteria (Euclid, Elements Book I, Propositions 8 and 26):

ASA: two angles and the side between them determine the triangle;
SSS: three sides determine the triangle.

From ASA and the angle sum of a triangle (proved below) follows AAS. But two famous combinations are not criteria: AAA only gives similar triangles (the same shape, perhaps a different size), and SSA fails, as we will see.

Definition— parallel lines

Two lines in a plane are parallel if they do not meet, however far they are extended.

Definition— Playfair's axiom (the parallel postulate)

Through a point not on a given line there is exactly one line parallel to the given line.

Playfair's axiom (popularised by John Playfair in 1795, though it was known much earlier) is equivalent to Euclid's fifth postulate, given the other axioms, and is easier to use.

When a line $t$ , a transversal, crosses two lines $\ell$ and $m$ , it makes eight angles. Two angles on opposite sides of $t$ and between $\ell$ and $m$ are called alternate angles.

Definition— circle words

A circle with centre $O$ and radius $r$ is the set of points at distance $r$ from $O$ . A chord joins two points of the circle; a diameter is a chord through $O$ . For a chord $AC$ :

the central angle is $\angle AOC$ ;
an inscribed angle is $\angle ABC$ where $B$ is another point of the circle. Its vertex is on the circle and its sides are chords. We say it subtends the arc $AC$ that does not contain $B$ .

Definition— perpendicular bisector and circumcentre

The perpendicular bisector of a segment $AB$ is the line through the midpoint of $AB$ perpendicular to $AB$ . A circle through all three vertices of a triangle is its circumcircle, and its centre is the circumcentre.

Worked examplesH

Proofs with congruent triangles

The best way to learn to write geometric proofs is to read and write short ones. In each proof below, every step names its reason.

Example— The isosceles triangle theorem

Claim. If $AB = AC$ in triangle $ABC$ , then $\angle B = \angle C$ .

Proof. Compare triangle $ABC$ with itself, read in a different order: triangle $ACB$ . We have $AB = AC$ and $AC = AB$ (given), and the included angles $\angle BAC$ and $\angle CAB$ are the same angle. By SAS, $\triangle ABC \cong \triangle ACB$ . Corresponding angles are equal, so $\angle ABC = \angle ACB$ . $\blacksquare$

This elegant proof is credited to Pappus of Alexandria (4th century CE). Euclid's own proof (Book I, Proposition 5) uses a more complicated figure, and medieval students nicknamed it the pons asinorum, the "bridge of donkeys".

Example— Opposite sides of a parallelogram

A parallelogram is a quadrilateral $ABCD$ with $AB \parallel DC$ and $AD \parallel BC$ .

Claim. In a parallelogram, $AB = DC$ and $AD = BC$ .

Proof. Draw the diagonal $AC$ . Since $AB \parallel DC$ and $AC$ is a transversal, the alternate angles are equal: $\angle BAC = \angle DCA$ . Since $AD \parallel BC$ , also $\angle DAC = \angle BCA$ . The side $AC$ is shared. By ASA, $\triangle ABC \cong \triangle CDA$ , so $AB = CD$ and $BC = DA$ . $\blacksquare$

The step "alternate angles are equal" uses the parallel postulate; see the next section.

Example— The carpenter's diagonal test

Claim. If a parallelogram $ABCD$ has equal diagonals, $AC = BD$ , then it is a rectangle.

Proof. Compare triangles $DAB$ and $CBA$ . They share the side $AB$ , $AD = BC$ (opposite sides of a parallelogram, just proved) and $BD = AC$ (given). By SSS, $\triangle DAB \cong \triangle CBA$ , so $\angle DAB = \angle CBA$ . But $AD \parallel BC$ , so these two angles are co-interior angles on the transversal $AB$ and add up to $180^\circ$ . Two equal angles with sum $180^\circ$ are each $90^\circ$ . The opposite angles of a parallelogram are equal (by the congruence $\triangle ABC \cong \triangle CDA$ above), so all four angles are right angles. $\blacksquare$

So the carpenter is right, provided her frame is a parallelogram — which it is, because she made opposite sides equal. (A quadrilateral that does not cross itself and has both pairs of opposite sides equal is a parallelogram: draw the diagonal $AC$ , use SSS to get $\triangle ABC \cong \triangle CDA$ , and then the equal alternate angles $\angle BAC = \angle DCA$ give $AB \parallel DC$ by Proposition I.27 below.)

Example— A non-example: SSA

Two sides and an angle that is not between them do not determine a triangle. Put $A = (0, 0)$ , $B = (4, 3)$ , $C = (3, 0)$ and $C' = (5, 0)$ . Then

$AB = 5$ in both triangles $ABC$ and $ABC'$ ;
$BC = \sqrt{1^2 + 3^2} = \sqrt{10}$ and $BC' = \sqrt{1^2 + 3^2} = \sqrt{10}$ ;
the angle at $A$ is the same, because $C$ and $C'$ lie on the same ray from $A$ .

But $AC = 3$ and $AC' = 5$ , so the triangles are not congruent.

The ambiguous case. The circle with centre B and radius √10 meets the ray from A in two points, C and C′. Triangles ABC and ABC′ share two sides and the angle at A, but they are not congruent.

When exactly does this happen? Let the angle at $A$ be acute, let $AB = c$ and $BC = a$ , and let $F$ be the foot of the perpendicular from $B$ to the line through $A$ and $C$ , with $BF = h$ . A point $X$ of that line has $BX = a$ exactly when $FX = \sqrt{a^2 - h^2}$ , by Pythagoras. So there is no such point if $a \lt h$ , one (namely $F$ , giving a right angle at $C$ ) if $a = h$ , and two, one on each side of $F$ , if $a > h$ . Both lie on the ray from $A$ exactly when $\sqrt{a^2 - h^2} \lt AF = \sqrt{c^2 - h^2}$ , that is, when $a \lt c$ . So SSA gives two different triangles exactly when $h \lt a \lt c$ . If the angle at $A$ is right or obtuse, at most one point lies on the ray, so SSA does determine the triangle — a fact sometimes called the hypotenuse–leg (or RHS) criterion when the angle is right.

ProofH

Parallel lines and the angle sum

The next theorem is proved without the parallel postulate. It rests on the exterior angle inequality (Euclid I.16): an exterior angle of a triangle is greater than each of the two interior angles not next to it. Euclid's proof of I.16 uses SAS and vertical angles, not the parallel postulate; we take it as known.

Theorem— Proposition (Euclid I.27)

If a transversal makes equal alternate angles with two lines, the lines are parallel.

Proof

Suppose the transversal crosses $\ell$ at $P$ and $m$ at $Q$ , with equal alternate angles, and suppose $\ell$ and $m$ meet at a point $R$ . Then $P$ , $Q$ , $R$ form a triangle. One of the two alternate angles is an interior angle of this triangle, and the other is an exterior angle at the other end of $PQ$ . By the exterior angle inequality, the exterior angle is greater than that interior angle — but they are equal. This contradiction shows that $\ell$ and $m$ do not meet. $\blacksquare$

∎

Theorem— Theorem (alternate angles)

If two parallel lines are crossed by a transversal, then alternate angles are equal.

Proof

Let $\ell \parallel m$ , and let the transversal cross them at $P$ and $Q$ . Through $P$ draw the line $\ell'$ that makes an alternate angle with $m$ equal to the one at $Q$ . By Proposition I.27, $\ell'$ is parallel to $m$ . Now $\ell$ and $\ell'$ are both lines through $P$ parallel to $m$ . By Playfair's axiom, there is only one, so $\ell = \ell'$ , and the alternate angles made by $\ell$ are equal. $\blacksquare$

∎

Theorem— Theorem (angle sum of a triangle)

The angles of every triangle add up to $180^\circ$ .

Proof

Let the triangle be $ABC$ , with angles $\alpha$ at $A$ , $\beta$ at $B$ and $\gamma$ at $C$ . Through $C$ draw the line $\ell$ parallel to $AB$ (it exists, and is unique, by Playfair's axiom). The line $CA$ is a transversal of the parallel lines $\ell$ and $AB$ , so the angle between $\ell$ and $CA$ on the side of $A$ equals $\alpha$ (alternate angles). In the same way, the angle between $\ell$ and $CB$ on the other side equals $\beta$ . These two angles and $\gamma$ fill the straight angle at $C$ along $\ell$ , so $\alpha + \gamma + \beta = 180^\circ$ . $\blacksquare$

∎

The line through C parallel to AB. Alternate angles copy α and β up to C, where they sit beside γ on a straight line: α + β + γ = 180°.

Theorem— Corollaries

Exterior angle theorem. An exterior angle of a triangle equals the sum of the two interior angles not next to it.
Polygons. The interior angles of a convex polygon with $n$ sides add up to $(n - 2) \cdot 180^\circ$ .

Proof

The exterior angle at $C$ and $\gamma$ lie on a straight line, so the exterior angle is $180^\circ - \gamma = \alpha + \beta$ .
The diagonals from one vertex cut the polygon into $n - 2$ triangles, whose angles together make up exactly the angles of the polygon. Each triangle contributes $180^\circ$ . $\blacksquare$

∎

Note

The exterior angle inequality (I.16) holds without the parallel postulate; the exterior angle theorem (an equality) needs it. On a sphere, where lines are great circles and there are no parallels at all, the angles of a triangle add up to more than $180^\circ$ . In the hyperbolic plane, where there are infinitely many parallels through a point, they add up to less. In fact, given the other axioms (including Archimedes' axiom about lengths), "every triangle has angle sum $180^\circ$ " is equivalent to the parallel postulate.

ProofH

Circles: the inscribed angle theorem

Theorem— Inscribed angle theorem

An inscribed angle is half the central angle subtending the same arc: if $A$ , $B$ , $C$ lie on a circle with centre $O$ , and $B$ lies on the same side of the line $AC$ as $O$ (or $O$ lies on $AC$ ), then $\angle AOC = 2\,\angle ABC$ .

Proof

Case 1: the centre lies on a side of the inscribed angle, say on $BC$ , so $BC$ is a diameter. The triangle $OAB$ is isosceles, since $OA = OB$ (both are radii). By the isosceles triangle theorem, $\angle OAB = \angle OBA = \theta$ , say. The angle $\angle AOC$ is an exterior angle of triangle $OAB$ (because $B$ , $O$ , $C$ lie on a line), so by the exterior angle theorem $\angle AOC = \theta + \theta = 2\theta = 2\,\angle ABC$ .

Case 2: the centre lies inside the angle $\angle ABC$ . Draw the diameter $BD$ through $O$ . It splits both angles: $\angle ABC = \angle ABD + \angle DBC$ and $\angle AOC = \angle AOD + \angle DOC$ . By Case 1, applied twice, $\angle AOD = 2\,\angle ABD$ and $\angle DOC = 2\,\angle DBC$ . Adding gives $\angle AOC = 2\,\angle ABC$ .

Case 3: the centre lies outside the angle $\angle ABC$ (but on the same side of $AC$ as $B$ ). Again draw the diameter $BD$ . Now one angle is the difference of two, say $\angle ABC = \angle DBC - \angle DBA$ and $\angle AOC = \angle DOC - \angle DOA$ . Subtracting the two instances of Case 1 gives the result. $\blacksquare$

∎

The inscribed angle θ at B and the central angle 2θ at O stand on the same arc AC. The dashed diameter through B is the one used in Cases 2 and 3 of the proof.

If $B$ is on the other side of $AC$ from $O$ , the same argument shows that $\angle ABC$ is half the reflex central angle, $360^\circ - \angle AOC$ . Three corollaries follow at once.

Theorem— Corollaries

Thales' theorem. An angle inscribed in a semicircle is a right angle: if $AC$ is a diameter and $B$ is on the circle, then $\angle ABC = 90^\circ$ .
Angles in the same segment. Inscribed angles subtending the same arc are equal.
Cyclic quadrilaterals. If the four vertices of a quadrilateral $ABCD$ lie on a circle (in this order), its opposite angles add up to $180^\circ$ .

Proof

The central angle is the straight angle $\angle AOC = 180^\circ$ , so $\angle ABC = 90^\circ$ .
Each is half of the same central angle.
$\angle ABC$ and $\angle ADC$ subtend the two arcs into which $A$ and $C$ cut the circle. Their central angles add up to $360^\circ$ , so the inscribed angles add up to $180^\circ$ . $\blacksquare$

∎

ProofH

The circumcentre

Theorem— Lemma (the perpendicular bisector as a locus)

A point $P$ is equidistant from $A$ and $B$ if and only if $P$ lies on the perpendicular bisector of $AB$ .

Proof

Let $M$ be the midpoint of $AB$ . If $P = M$ there is nothing to prove, so let $P \ne M$ .

If $P$ is on the perpendicular bisector, then triangles $PMA$ and $PMB$ have $MA = MB$ , a common side $PM$ , and right angles at $M$ . By SAS they are congruent, so $PA = PB$ .

Conversely, if $PA = PB$ , then triangles $PMA$ and $PMB$ have three equal sides, so by SSS they are congruent. Hence $\angle PMA = \angle PMB$ . These two angles lie on a straight line, so each is $90^\circ$ , and $PM$ is the perpendicular bisector. $\blacksquare$

∎

Theorem— Theorem (circumcentre)

The three perpendicular bisectors of the sides of a triangle $ABC$ meet in a single point $O$ , and the circle with centre $O$ through $A$ passes through $B$ and $C$ .

Proof

First, the perpendicular bisectors of $AB$ and $BC$ meet. Suppose instead that they were parallel. The line $AB$ is perpendicular to the first bisector, so it crosses it, and therefore (by Playfair's axiom) it also crosses the second; by the alternate angles theorem it is perpendicular to the second bisector as well. So $AB$ and $BC$ would both be perpendicular to the second bisector. Two lines perpendicular to the same line are parallel or equal (Proposition I.27), and $AB$ and $BC$ share the point $B$ , so they would be the same line: $A$ , $B$ , $C$ would be collinear, which is not a triangle. This step uses the parallel postulate.

Let $O$ be the meeting point. By the lemma, $OA = OB$ (as $O$ is on the bisector of $AB$ ) and $OB = OC$ (as $O$ is on the bisector of $BC$ ). So $OA = OC$ , and by the lemma again $O$ lies on the perpendicular bisector of $CA$ . All three bisectors pass through $O$ , and $OA = OB = OC$ is the radius of a circle through all three vertices. $\blacksquare$

∎

The parallel postulate really is needed here. In the hyperbolic plane there are triangles whose perpendicular bisectors never meet, so they have no circumcircle; in fact, given Hilbert's other axioms, "every triangle has a circumcircle" is equivalent to the parallel postulate. Farkas Bolyai, the father of János Bolyai, gave an attempted proof of the parallel postulate that relied, without noticing, on this equivalent statement.

Note

The isosceles "proof", resolved. The bisector of the angle at $A$ and the perpendicular bisector of $BC$ do meet — but, unless $AB = AC$ , they meet on the circumcircle, at the midpoint of the arc $BC$ that does not contain $A$ . That point is outside the triangle. When the figure is drawn correctly, one of the two feet of the perpendiculars from $P$ lands on a side and the other on an extended side, and the final step of the "proof" (adding equal pieces on one side, but subtracting them on the other) no longer gives $AB = AC$ . A careful proof would have had to justify where $P$ lies, and it cannot.

Formal mathematicsF

Euclid in Lean

Mathlib, Lean's mathematical library, does not start from Euclid's axioms. It builds the plane out of vectors: points can be subtracted to give displacement vectors, and an inner product (dot product) on the vectors gives lengths and angles. In this model Euclid's axioms are theorems. Here is Playfair's axiom, proved in Lean. (In Mathlib a line counts as parallel to itself, which is why the statement does not need $p \notin s$ .)

playfairLean 4Proved here from basic factsFormally verified

/-- **Playfair's axiom holds in the model.** Through a point `p` there is exactly one affine
subspace parallel to a given non-empty one `s` (for a line `s`: exactly one line through `p`
parallel to `s`). Mathlib's `s ∥ t` means that `t` is a translate of `s`, so a line counts as
parallel to itself. Existence: the translate of `s` through `p`, `mk' p s.direction`.
Uniqueness: a parallel `t` has the same direction as `s`, and an affine subspace is determined
by its direction and one of its points (`AffineSubspace.mk'_eq`). In Hilbert's axioms this is
an *axiom*; in the vector model it is a *theorem*. -/
theorem playfair (s : AffineSubspace ℝ P) (hs : s ≠ ⊥) (p : P) :
    ∃! t : AffineSubspace ℝ P, p ∈ t ∧ t ∥ s := by
  have hne : AffineSubspace.mk' p s.direction ≠ ⊥ :=
    (AffineSubspace.nonempty_iff_ne_bot _).1 ⟨p, AffineSubspace.self_mem_mk' p s.direction⟩
  refine ⟨AffineSubspace.mk' p s.direction, ⟨AffineSubspace.self_mem_mk' p s.direction, ?_⟩, ?_⟩
  · rw [AffineSubspace.parallel_iff_direction_eq_and_eq_bot_iff_eq_bot]
    exact ⟨AffineSubspace.direction_mk' p s.direction, ⟨fun h => absurd h hne, fun h => absurd h hs⟩⟩
  · rintro t ⟨hpt, hts⟩
    rw [← hts.direction_eq]
    exact (AffineSubspace.mk'_eq hpt).symm