Book I · Proposition 38

I.38

Triangles which are on equal bases and in the same parallels are equal to one another.Heath, 1908
ABCDEF
24 lines and circles drawn, of which 8 helper constructions drew the fainter ones

Every step, checked

What it needs, and what needs it

Needs: I.31 I.34 I.36

Used by: I.40 I.42 VI.1 VI.2

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

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

What it takes on trust

The proposition as code

@proposition(
    "I.38",
    THEOREM,
    sample=samples.triangles_equal_bases,
)
def prop_I_38(a: Point, b: Point, c: Point, d: Point, e: Point, f: Point) -> Out:
    hypothesis("the bases AB and DE are equal", eq_len(a, b, d, e))
    hypothesis("the bases lie on one straight line", collinear(a, b, d) and collinear(a, b, e))
    # Euclid names the parallel by joining the apexes, which needs two of them,
    # and the commonest use of I.38 has one: I.42 compares ABE with AEC, and
    # every triangle standing on a cut base in Book VI stands on the same point.
    # The parallel through C is that line whether or not F is C, so I.31 draws
    # it and F is asked to lie on it. Naming it by the join instead cost five
    # citations, which were left recorded but unrun.
    through_apexes = _parallel_through(c, a, b)
    hypothesis("the apexes lie on one parallel to the bases", on_line(f, through_apexes))
    outline(a, b, c)
    outline(d, e, f)
    if c != f:
        line(c, f, "the parallel through the apexes")

    top_c, top_f = _fourth_vertex(b, a, c), _fourth_vertex(e, d, f)
    because(prop_I_36, a, b, c, top_c, d, e, f, top_f)
    because(prop_I_34, a, b, c, top_c)

    claim("the completed parallelograms on equal bases are equal", "I.36",
          eq_polygon_area(
              [a, b, c, _fourth_vertex(b, a, c)], [d, e, f, _fourth_vertex(e, d, f)]))
    claim("and each triangle is half of its parallelogram", "I.34",
          eq_area((a, b, c), (d, e, f)))
    return Out()