Book I · Proposition 40

I.40

Equal triangles which are on equal bases and on the same side are also in the same parallels.Heath, 1908

Every step, checked

• the bases are equal and in one straight linegiven
• C and F are on the same sidegiven
• the triangles are equalgiven
• were CF not parallel to the bases, I.38 would make a part equal the wholeby I.38

What it needs, and what needs it

Needs: I.31 I.38

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: 14 steps of argument above the first principles. Parallel postulate: needed.

What it takes on trust

• a circle-circle intersection is used, though no postulate asserts that two circles meet (×2)continuity
• a line-circle intersection is used, though no postulate asserts that a line meets a circle (×2)continuity
• the argument reads a 'same_side' fact off the figureorder

The proposition as code

@proposition(
    "I.40",
    THEOREM,
    sample=_equal_triangles_equal_bases,
)
def prop_I_40(a: Point, b: Point, c: Point, d: Point, e: Point, f: Point) -> Out:
    hypothesis("the bases are equal and in one straight line",
               eq_len(a, b, d, e) and collinear(a, b, d) and collinear(a, b, e))
    hypothesis("C and F are on the same side", same_side(c, f, Line.through(a, b)))
    hypothesis("the triangles are equal", eq_area((a, b, c), (d, e, f)))
    outline(a, b, c)
    outline(d, e, f)
    line(c, f)

    alongside = prop_I_31(c, a, b).parallel
    cut = meet_one(alongside, Line.through(e, f))
    because(prop_I_38, a, b, c, d, e, cut)

    claim("were CF not parallel to the bases, I.38 would make a part equal the whole", "I.38",
          parallel(Line.through(c, f), Line.through(a, b)))
    return Out()