Book I · Proposition 29

I.29

A straight line falling on parallel straight lines makes the alternate angles equal to one another, the exterior angle equal to the interior and opposite angle, and the interior angles on the same side equal to two right angles.Heath, 1908

The first proposition in the Elements that needs the parallel postulate.

Every step, checked

• G lies on AB and H on CDgiven
• AB is parallel to CDgiven
• were the alternate angles unequal, the interior angles on one side would sum to less than two right angles, and by Postulate 5 the lines would meetby Post.5, I.13
• the exterior angle BGH equals the interior and opposite angle GHD's supplementby I.15
• and the interior angles on the same side sum to two right anglesby I.13

What it needs, and what needs it

Needs: I.13 I.15

Used by: I.30 I.32 I.33 I.34

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

Depth: 2 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.29",
    THEOREM,
    sample=_transversal,
    note="The first proposition in the Elements that needs the parallel postulate.",
)
def prop_I_29(a: Point, b: Point, c: Point, d: Point, g: Point, h: Point) -> Out:
    first, second = line(a, b, "AB"), line(c, d, "CD")
    line(g, h, "the transversal GH")
    hypothesis("G lies on AB and H on CD", on_line(g, first) and on_line(h, second))
    hypothesis("AB is parallel to CD", parallel(first, second))

    # I.13 and I.15 speak of a line standing within another, so each line is
    # taken on both sides of the point the transversal crosses it at. G may be
    # an end of AB -- I.32 hands it the vertex -- and then A and B alone will
    # not do.
    span, across = (b.x - a.x, b.y - a.y), (d.x - c.x, d.y - c.y)
    before_g = Point(g.x - span[0], g.y - span[1])
    after_g = Point(g.x + span[0], g.y + span[1])
    before_h = Point(h.x - across[0], h.y - across[1])
    after_h = Point(h.x + across[0], h.y + across[1])
    beyond = posit(Point(g.x + (g.x - h.x), g.y + (g.y - h.y)), "K")
    line(beyond, h, "the transversal produced to K")
    because(prop_I_13, before_g, g, after_g, h)
    because(prop_I_13, before_h, h, after_h, g)
    because(prop_I_15, before_g, after_g, beyond, h)

    claim("were the alternate angles unequal, the interior angles on one side would sum "
          "to less than two right angles, and by Postulate 5 the lines would meet",
          ["Post.5", "I.13"], eq_angle(a, g, h, g, h, d))
    claim("the exterior angle BGH equals the interior and opposite angle GHD's supplement",
          "I.15", eq_angle(b, g, h, g, h, c))
    claim("and the interior angles on the same side sum to two right angles", "I.13",
          angle_at(b, g, h) + angle_at(g, h, d) == STRAIGHT)
    return Out()