Book I · Proposition 18

I.18

In any triangle the greater side subtends the greater angle.Heath, 1908

Every step, checked

• ABC is a genuine trianglegiven
• AC is greater than ABgiven
• cutting AD equal to AB from the greater side and using I.5 and I.16, the angle ABC exceeds the angle BCAby I.3, I.5, I.16

What it needs, and what needs it

Needs: I.3 I.5 I.16

Used by: I.19 III.2

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

The proposition as code

@proposition(
    "I.18",
    THEOREM,
    sample=_unequal_sides,
)
def prop_I_18(a: Point, b: Point, c: Point) -> Out:
    hypothesis("ABC is a genuine triangle", not collinear(a, b, c), guard=True)
    hypothesis("AC is greater than AB", len2(a, c) > len2(a, b))
    outline(a, b, c)

    # AD is cut off from AC equal to AB, BD joined: ABD is then isosceles and
    # ADB is exterior to BDC. The lesser line is named BA, since I.3 places it
    # at A through I.2 and I.2 joins the point to an end of the line.
    d = posit(prop_I_3(a, c, b, a).cut, "D")
    line(b, d, "join BD")
    because(prop_I_5, a, b, d)
    because(prop_I_16, b, c, d)

    claim("cutting AD equal to AB from the greater side and using I.5 and I.16, "
          "the angle ABC exceeds the angle BCA", ["I.3", "I.5", "I.16"],
          angle_cmp(a, b, c, b, c, a) > 0)
    return Out()