Book I · Proposition 16

I.16

In any triangle, if one of the sides be produced, the exterior angle is greater than either of the interior and opposite angles.Heath, 1908

Euclid's proof needs the produced line to fall where the diagram shows it -- a betweenness assumption the postulates do not supply. It is the classic example of a step that fails on a sphere.

Every step, checked

• ABC is a genuine trianglegiven
• AE = EC and BE = EF by constructionby I.10
• the vertical angles at E are equalby I.15
• so triangles AEB and CEF are equal, giving angle BAE = angle ECFby I.4
• the exterior angle ACD exceeds the interior and opposite angle BACby C.N.5
• and likewise it exceeds the angle ABCby C.N.5

What it needs, and what needs it

Needs: I.4 I.10 I.15

Used by: I.17 I.18 I.21 I.26 I.27

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

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

What it takes on trust

• a circle-circle intersection is used, though no postulate asserts that two circles meet (×4)continuity
• a line-circle intersection is used, though no postulate asserts that a line meets a circle (×4)continuity

The proposition as code

@proposition(
    "I.16",
    THEOREM,
    sample=samples.triangle,
    note="Euclid's proof needs the produced line to fall where the diagram shows it -- "
    "a betweenness assumption the postulates do not supply. It is the classic example "
    "of a step that fails on a sphere.",
)
def prop_I_16(a: Point, b: Point, c: Point) -> Out:
    hypothesis("ABC is a genuine triangle", not collinear(a, b, c), guard=True)

    # produce BC to D
    d = posit(Point(c.x + (c.x - b.x), c.y + (c.y - b.y)), "D")
    line(b, d, "BC produced to D")
    middle = posit(prop_I_10(a, c).midpoint, "E")
    f = posit(Point(middle.x + (middle.x - b.x), middle.y + (middle.y - b.y)), "F")
    line(b, f, "BE produced to F")

    claim("AE = EC and BE = EF by construction", "I.10",
          eq_len(a, middle, middle, c) and eq_len(b, middle, middle, f))
    because(prop_I_15, a, c, b, f)
    because(prop_I_4, middle, a, b, middle, c, f)

    claim("the vertical angles at E are equal", "I.15",
          eq_angle(a, middle, b, c, middle, f))
    claim("so triangles AEB and CEF are equal, giving angle BAE = angle ECF", "I.4",
          eq_angle(b, a, middle, middle, c, f))
    claim("the exterior angle ACD exceeds the interior and opposite angle BAC", "C.N.5",
          angle_at(a, c, d) > angle_at(b, a, c))
    claim("and likewise it exceeds the angle ABC", "C.N.5",
          angle_at(a, c, d) > angle_at(a, b, c))
    return Out(produced=d)