Book I · Proposition 26

I.26

If two triangles have the two angles equal to two angles respectively, and one side equal to one side, namely, either the side adjoining the equal angles, or that subtending one of the equal angles, they will also have the remaining sides equal to the remaining sides and the remaining angle to the remaining angle.Heath, 1908

Angle-side-angle, and angle-angle-side.

Every step, checked

• angle ABC = angle DEFgiven
• angle BCA = angle EFDgiven
• the adjoining side BC = EFgiven
• were AB unequal to DE, cutting off an equal part and applying I.4 would make the exterior angle equal to the interior and opposite, contrary to I.16; so AB = DEby I.4, I.16
• hence also AC = DFby I.4
• and the remaining angle BAC equals the remaining angle EDFby I.4

What it needs, and what needs it

Needs: I.4 I.16

Used by: I.34 IV.4

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

The proposition as code

@proposition(
    "I.26",
    THEOREM,
    sample=_asa_pair,
    note="Angle-side-angle, and angle-angle-side.",
)
def prop_I_26(a: Point, b: Point, c: Point, d: Point, e: Point, f: Point) -> Out:
    hypothesis("angle ABC = angle DEF", eq_angle(a, b, c, d, e, f))
    hypothesis("angle BCA = angle EFD", eq_angle(b, c, a, e, f, d))
    hypothesis("the adjoining side BC = EF", eq_len(b, c, e, f))
    outline(a, b, c)
    outline(d, e, f)
    # The part Euclid cuts off is AB itself once the sides prove equal, so the
    # triangle his reductio compares is this one, and I.16 speaks of it.
    because(prop_I_16, a, b, c)
    because(prop_I_4, b, a, c, e, d, f)

    claim("were AB unequal to DE, cutting off an equal part and applying I.4 would make "
          "the exterior angle equal to the interior and opposite, contrary to I.16; "
          "so AB = DE", ["I.4", "I.16"], eq_len(a, b, d, e))
    claim("hence also AC = DF", "I.4", eq_len(a, c, d, f))
    claim("and the remaining angle BAC equals the remaining angle EDF", "I.4",
          eq_angle(b, a, c, e, d, f))
    return Out()