Book I · Proposition 4

I.4

If two triangles have the two sides equal to two sides respectively, and have the angles contained by the equal straight lines equal, they will also have the base equal to the base, the triangle will be equal to the triangle, and the remaining angles will be equal to the remaining angles respectively, namely those which the equal sides subtend.Heath, 1908

Side-angle-side. Euclid argues by superposition; the machine checks the conclusion exactly on every sampled configuration meeting the hypothesis.

Every step, checked

• AB = DEgiven
• AC = DFgiven
• the included angles BAC and EDF are equalgiven
• the base BC equals the base EFby Def.4
• the triangles are equal in areaby C.N.4
• angle ABC = angle DEFby C.N.4
• angle ACB = angle DFEby C.N.4

What it needs, and what needs it

Needs: nothing earlier.

Used by: I.5 I.6 I.10 I.16 I.24 I.25 I.26 I.33 I.34 I.35 I.47 III.17 III.24 III.26 III.29 III.30 IV.6 IV.13 VI.6 XI.22 XIII.7

Rests on: C.N.4, Def.4

Depth: 0 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.4",
    THEOREM,
    sample=_sas_pair,
    note="Side-angle-side. Euclid argues by superposition; the machine checks the "
    "conclusion exactly on every sampled configuration meeting the hypothesis.",
)
def prop_I_4(a: Point, b: Point, c: Point, d: Point, e: Point, f: Point) -> Out:
    hypothesis("AB = DE", eq_len(a, b, d, e))
    hypothesis("AC = DF", eq_len(a, c, d, f))
    hypothesis("the included angles BAC and EDF are equal", eq_angle(b, a, c, e, d, f))
    outline(a, b, c)
    outline(d, e, f)

    claim("the base BC equals the base EF", "Def.4", eq_len(b, c, e, f))
    claim("the triangles are equal in area", "C.N.4", eq_area((a, b, c), (d, e, f)))
    claim("angle ABC = angle DEF", "C.N.4", eq_angle(a, b, c, d, e, f))
    claim("angle ACB = angle DFE", "C.N.4", eq_angle(a, c, b, d, f, e))
    return Out()