Book I · Proposition 33

I.33

The straight lines joining equal and parallel straight lines (at the extremities which are) in the same directions (respectively) are themselves also equal and parallel.Heath, 1908

Every step, checked

• AB equals DCgiven
• AB is parallel to DCgiven
• the alternate angles BAC and ACD are equalby I.29
• so the triangles ABC and CDA are equal, giving AD = BCby I.4
• and the alternate angles being equal, AD is parallel to BCby I.27

What it needs, and what needs it

Needs: I.4 I.27 I.29

Used by: I.36 VI.32

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

Depth: 10 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.33",
    THEOREM,
    sample=samples.parallelogram,
)
def prop_I_33(a: Point, b: Point, c: Point, d: Point) -> Out:
    hypothesis("AB equals DC", eq_len(a, b, d, c))
    hypothesis("AB is parallel to DC", parallel(Line.through(a, b), Line.through(d, c)))
    joined_one, joined_two = line(a, d, "AD"), line(b, c, "BC")
    line(a, c, "the diagonal AC")

    # AC crosses each pair of lines at an end of itself, so each is named by
    # points straddling the crossing -- the same care I.29 and I.27 want.
    back_a, back_c = Point(2 * a.x - b.x, 2 * a.y - b.y), Point(2 * c.x - d.x, 2 * c.y - d.y)
    off_a, off_c = Point(2 * a.x - d.x, 2 * a.y - d.y), Point(2 * c.x - b.x, 2 * c.y - b.y)
    because(prop_I_29, b, back_a, back_c, d, a, c)
    because(prop_I_4, a, b, c, c, d, a)
    because(prop_I_27, d, off_a, off_c, b, a, c)

    claim("the alternate angles BAC and ACD are equal", "I.29", eq_angle(b, a, c, a, c, d))
    claim("so the triangles ABC and CDA are equal, giving AD = BC", "I.4", eq_len(a, d, b, c))
    claim("and the alternate angles being equal, AD is parallel to BC", "I.27",
          parallel(joined_one, joined_two))
    return Out()