Book I · Proposition 17

I.17

In any triangle two angles taken together in any manner are less than two right angles.Heath, 1908

Every step, checked

• ABC is a genuine trianglegiven
• angle A and angle B together fall short of two right anglesby I.16
• so do angle B and angle Cby I.16
• and so do angle C and angle Aby I.16

What it needs, and what needs it

Needs: I.16

Used by: III.16

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

Depth: 9 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 (×12)continuity
• a line-circle intersection is used, though no postulate asserts that a line meets a circle (×12)continuity

The proposition as code

@proposition(
    "I.17",
    THEOREM,
    sample=samples.triangle,
)
def prop_I_17(a: Point, b: Point, c: Point) -> Out:
    hypothesis("ABC is a genuine triangle", not collinear(a, b, c), guard=True)
    outline(a, b, c)
    alpha, beta, gamma = angle_at(b, a, c), angle_at(a, b, c), angle_at(a, c, b)

    # Each pair wants its own side produced, and the exterior angle so made is
    # I.16's business. Three applications, one per pair.
    because(prop_I_16, c, a, b)
    because(prop_I_16, a, b, c)
    because(prop_I_16, b, c, a)

    claim("angle A and angle B together fall short of two right angles", "I.16",
          alpha + beta < STRAIGHT)
    claim("so do angle B and angle C", "I.16", beta + gamma < STRAIGHT)
    claim("and so do angle C and angle A", "I.16", gamma + alpha < STRAIGHT)
    return Out()