Book I · Proposition 38
Triangles which are on equal bases and in the same parallels are equal to one another.Heath, 1908
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.
@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()