Book I · Proposition 25

I.25

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

Every step, checked

• AB = DE and AC = DFgiven
• the base BC is greater than the base EFgiven
• were the angle at A not greater, I.4 or I.24 would contradict the basesby I.4, I.24

What it needs, and what needs it

Needs: I.4 I.24

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

Depth: 12 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.25",
    THEOREM,
    sample=_hinge_pair,
)
def prop_I_25(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 base BC is greater than the base EF", len2(b, c) > len2(e, f))
    # I.24 is this proposition read the other way, and its hypotheses hold of
    # the figure in hand. The case Euclid excludes, the angles being equal, is
    # I.4's, and no figure meeting this hypothesis has it.
    because(prop_I_24, a, b, c, d, e, f)

    claim("were the angle at A not greater, I.4 or I.24 would contradict the bases",
          ["I.4", "I.24"], angle_cmp(b, a, c, e, d, f) > 0)
    return Out()