Book I · Proposition 8

I.8

If two triangles have the two sides equal to two sides respectively, and have also the base equal to the base, they will also have the angles equal which are contained by the equal straight lines.Heath, 1908

Every step, checked

• the three sides are equal respectivelygiven
• applying one triangle to the other, I.7 forbids the apexes to differ, so angle BAC = angle EDFby I.7
• likewise angle ABC = angle DEFby I.7
• and angle BCA = angle EFDby I.7

What it needs, and what needs it

Needs: I.7

Used by: I.9 I.11 I.12 I.22 I.23 I.48 III.3 III.26 III.28 IV.12 VI.5

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

Depth: 5 steps of argument above the first principles. Parallel postulate: not needed.

What it takes on trust

Nothing. It draws no intersections and reads nothing off the picture.

The proposition as code

@proposition(
    "I.8",
    THEOREM,
    sample=_sss_pair,
)
def prop_I_8(a: Point, b: Point, c: Point, d: Point, e: Point, f: Point) -> Out:
    hypothesis("the three sides are equal respectively", congruent_sss((a, b, c), (d, e, f)))
    outline(a, b, c)
    outline(d, e, f)

    # Apply DEF to ABC, DE upon AB, and ask I.7 whether the apexes can differ.
    landed = _applied(d, e, f, a, b, beside=c)
    because(prop_I_7, a, b, c, landed)

    claim("applying one triangle to the other, I.7 forbids the apexes to differ, "
          "so angle BAC = angle EDF", "I.7",
          landed == c and eq_angle(b, a, c, e, d, f))
    claim("likewise angle ABC = angle DEF", "I.7", eq_angle(a, b, c, d, e, f))
    claim("and angle BCA = angle EFD", "I.7", eq_angle(b, c, a, e, f, d))
    return Out()