Book I · Proposition 32

I.32

In any triangle, if one of the sides be produced, the exterior angle is equal to the two interior and opposite angles, and the three interior angles of the triangle are equal to two right angles.Heath, 1908

Every step, checked

• ABC is a genuine trianglegiven
• the exterior angle ACD equals the sum of the angles at A and Bby I.29
• adding the angle at C, the three angles equal two right anglesby I.13

What it needs, and what needs it

Needs: I.13 I.29 I.31

Used by: III.20 VI.4

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

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

What it takes on trust

• a circle-circle intersection is used, though no postulate asserts that two circles meetcontinuity
• a line-circle intersection is used, though no postulate asserts that a line meets a circlecontinuity

The proposition as code

@proposition(
    "I.32",
    THEOREM,
    sample=samples.triangle,
)
def prop_I_32(a: Point, b: Point, c: Point) -> Out:
    hypothesis("ABC is a genuine triangle", not collinear(a, b, c), guard=True)
    d = posit(Point(c.x + (c.x - b.x), c.y + (c.y - b.y)), "D")
    line(b, d, "BC produced to D")
    alongside = prop_I_31(c, a, b).through

    # AC falls across AB and the parallel through C, meeting each at an end of
    # itself, so each line is named by two points straddling the crossing. The
    # alternate angle to BAC is on the far side of AC, which fixes which way
    # along the parallel to look.
    edge = Line.through(a, c)
    if edge.side_of(alongside) * edge.side_of(b) > 0:
        alongside = Point(2 * c.x - alongside.x, 2 * c.y - alongside.y)
    back_a = Point(2 * a.x - b.x, 2 * a.y - b.y)
    back_c = Point(2 * c.x - alongside.x, 2 * c.y - alongside.y)

    because(prop_I_29, b, back_a, back_c, alongside, a, c)
    because(prop_I_13, b, c, d, a)

    alpha, beta, gamma = angle_at(b, a, c), angle_at(a, b, c), angle_at(a, c, b)
    claim("the exterior angle ACD equals the sum of the angles at A and B", "I.29",
          angle_at(a, c, d) == alpha + beta)
    claim("adding the angle at C, the three angles equal two right angles", "I.13",
          alpha + beta + gamma == STRAIGHT)
    return Out(exterior=angle_at(a, c, d))