Book I · Proposition 19

I.19

In any triangle the greater angle is subtended by the greater side.Heath, 1908

Every step, checked

• ABC is a genuine trianglegiven
• the angle ABC is greater than the angle BCAgiven
• were AC not greater than AB, I.5 or I.18 would contradict the hypothesisby I.5, I.18

What it needs, and what needs it

Needs: I.5 I.18

Used by: I.20 I.24 III.16 III.18

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

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

The proposition as code

@proposition(
    "I.19",
    THEOREM,
    sample=_unequal_sides,
)
def prop_I_19(a: Point, b: Point, c: Point) -> Out:
    hypothesis("ABC is a genuine triangle", not collinear(a, b, c), guard=True)
    hypothesis("the angle ABC is greater than the angle BCA", angle_cmp(a, b, c, b, c, a) > 0)
    outline(a, b, c)

    # The case Euclid excludes is AB = AC, and no figure meeting this
    # hypothesis is isosceles, so I.5 cannot be applied to one. I.18 can: it is
    # this proposition read the other way, and it holds of the figure in hand.
    because(prop_I_18, a, b, c)

    claim("were AC not greater than AB, I.5 or I.18 would contradict the hypothesis",
          ["I.5", "I.18"], len2(a, c) > len2(a, b))
    return Out()