Book I · Proposition 36

I.36

Parallelograms which are on equal bases and in the same parallels are equal to one another.Heath, 1908

Every step, checked

• the bases AB and EF are equalgiven
• the bases lie on one straight linegiven
• the tops lie on one parallelgiven
• joining the ends of the equal and parallel bases gives a parallelogramby I.33
• both parallelograms equal that one, hence one anotherby I.35

What it needs, and what needs it

Needs: I.33 I.35

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

What it takes on trust

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

The proposition as code

@proposition(
    "I.36",
    THEOREM,
    sample=_parallelograms_equal_bases,
)
def prop_I_36(a: Point, b: Point, c: Point, d: Point, e: Point, f: Point, g: Point, h: Point) -> Out:
    hypothesis("the bases AB and EF are equal", eq_len(a, b, e, f))
    hypothesis("the bases lie on one straight line", collinear(a, b, e) and collinear(a, b, f))
    hypothesis("the tops lie on one parallel", collinear(d, c, g) and collinear(d, c, h))
    outline(a, b, c, d)
    outline(e, f, g, h)
    # AB and HG are equal and parallel, so joining their ends gives a third
    # parallelogram by I.33; each of the two then equals it by I.35, on the
    # base they share with it.
    because(prop_I_33, a, b, g, h)
    because(prop_I_35, a, b, c, d, g, h)
    because(prop_I_35, h, g, f, e, b, a)

    claim("joining the ends of the equal and parallel bases gives a parallelogram", "I.33",
          eq_len(a, b, e, f))
    claim("both parallelograms equal that one, hence one another", "I.35",
          eq_polygon_area([a, b, c, d], [e, f, g, h]))
    return Out()