Book I · Proposition 24

I.24

If two triangles have the two sides equal to two sides respectively, but have the one of the angles contained by the equal straight lines greater than the other, they will also have the base greater than the base.Heath, 1908

The hinge theorem.

Every step, checked

• AB = DE and AC = DFgiven
• the angle at A is greater than the angle at Dgiven
• the base BC is greater than the base EFby I.4, I.19

What it needs, and what needs it

Needs: I.4 I.19 I.23

Used by: I.25 III.7 III.8

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

Depth: 11 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 circlecontinuity

The proposition as code

@proposition(
    "I.24",
    THEOREM,
    sample=_hinge_pair,
    note="The hinge theorem.",
)
def prop_I_24(a: Point, b: Point, c: Point, d: Point, e: Point, f: Point) -> Out:
    hypothesis("AB = DE and AC = DF", eq_len(a, b, d, e) and eq_len(a, c, d, f))
    outline(a, b, c)
    outline(d, e, f)
    hypothesis("the angle at A is greater than the angle at D",
               angle_cmp(b, a, c, e, d, f) > 0)
    # At D on DE the angle BAC is copied, and DG made equal to DF. I.4 then
    # matches ABC with DEG, and I.19 compares EG with EF in the triangle EFG.
    copied = prop_I_23(b, a, c, d, e, beside=f)
    stretch = length(d, f) / length(d, copied.ray_through)
    g = posit(Point(d.x + stretch * (copied.ray_through.x - d.x),
                    d.y + stretch * (copied.ray_through.y - d.y)), "G")
    line(e, g, "join EG")
    line(f, g, "join FG")
    because(prop_I_4, a, b, c, d, e, g)
    because(prop_I_19, e, f, g)

    claim("the base BC is greater than the base EF", ["I.4", "I.19"], len2(b, c) > len2(e, f))
    return Out()