Book I · Proposition 20

I.20

In any triangle two sides taken together in any manner are greater than the remaining one.Heath, 1908

The triangle inequality -- which the Epicureans mocked as evident even to an ass.

ABC
12 lines and circles drawn, of which 15 helper constructions drew the fainter ones

Every step, checked

What it needs, and what needs it

Needs: I.5 I.19

Used by: I.21 III.7 III.8 III.11 III.12 III.15

Rests on: C.N.1, C.N.3, C.N.4, C.N.5, Def.10, Def.15, Def.4

Depth: 11 steps of argument above the first principles. Parallel postulate: not needed.

What it takes on trust

The proposition as code

@proposition(
    "I.20",
    THEOREM,
    sample=samples.triangle,
    note="The triangle inequality -- which the Epicureans mocked as evident even to an ass.",
)
def prop_I_20(a: Point, b: Point, c: Point) -> Out:
    hypothesis("ABC is a genuine triangle", not collinear(a, b, c), guard=True)
    outline(a, b, c)
    ab, bc, ca = length(a, b), length(b, c), length(c, a)

    # BA is produced to D with AD equal to AC, so ACD is isosceles and I.5
    # gives its base angles; the angle BCD then exceeds ADC, and I.19 turns
    # that into BD greater than BC. BD is BA and AC together.
    for near, far, apex in ((b, c, a), (c, a, b), (a, b, c)):
        reach = circle_with_radius2(apex, len2(apex, far),
                                    "circle centre the vertex, radius the far side")
        beyond = meet(line(near, apex), reach)[1]
        line(beyond, far)
        because(prop_I_5, apex, far, beyond)
        because(prop_I_19, near, far, beyond)

    claim("BA together with AC is greater than BC", ["I.5", "I.19"], ab + ca > bc)
    claim("AB together with BC is greater than AC", ["I.5", "I.19"], ab + bc > ca)
    claim("BC together with CA is greater than BA", ["I.5", "I.19"], bc + ca > ab)
    return Out()