Book I · Proposition 35

I.35

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

Every step, checked

What it needs, and what needs it

Needs: I.4 I.34

Used by: I.36 I.37 XI.31

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: 11 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.35",
    THEOREM,
    sample=samples.two_parallelograms_same_base,
)
def prop_I_35(a: Point, b: Point, c: Point, d: Point, e: Point, f: Point) -> Out:
    hypothesis("ABCD is a parallelogram",
               parallel(Line.through(a, b), Line.through(d, c))
               and parallel(Line.through(a, d), Line.through(b, c)))
    hypothesis("ABEF is a parallelogram on the same base",
               parallel(Line.through(a, b), Line.through(f, e))
               and parallel(Line.through(a, f), Line.through(b, e)))
    hypothesis("C, D, E, F lie on one parallel to AB",
               collinear(d, c, e) and collinear(d, c, f))
    outline(a, b, c, d)
    outline(a, b, e, f)

    because(prop_I_34, a, b, c, d)
    because(prop_I_34, a, b, e, f)
    because(prop_I_4, a, d, f, b, c, e)

    claim("AD = BC and AF = BE, the opposite sides", "I.34",
          eq_len(a, d, b, c) and eq_len(a, f, b, e))
    claim("DF = CE, adding or subtracting the common part", "C.N.2", eq_len(d, f, c, e))
    claim("so the triangles ADF and BCE are equal", "I.4", eq_area((a, d, f), (b, c, e)))
    claim("taking each from the trapezium, the parallelograms are equal", "C.N.3",
          eq_polygon_area([a, b, c, d], [a, b, e, f]))
    return Out()