Book I · Proposition 28

I.28

If a straight line falling on two straight lines make the exterior angle equal to the interior and opposite angle on the same side, or the interior angles on the same side equal to two right angles, the straight lines will be parallel to one another.Heath, 1908

Every step, checked

• G lies on AB and H on CDgiven
• the interior angles on the same side sum to two right anglesgiven
• the angle BGH is the supplement of AGHby I.13
• hence the alternate angles AGH and GHD are equalby C.N.3
• therefore AB is parallel to CDby I.27

What it needs, and what needs it

Needs: I.13 I.27

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

Depth: 10 steps of argument above the first principles. Parallel postulate: not needed.

What it takes on trust

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

The proposition as code

@proposition(
    "I.28",
    THEOREM,
    sample=_transversal,
)
def prop_I_28(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))
    interior = angle_at(b, g, h) + angle_at(g, h, d)
    hypothesis("the interior angles on the same side sum to two right angles",
               interior == STRAIGHT)

    span = (b.x - a.x, b.y - a.y)
    prop_I_13(Point(g.x - span[0], g.y - span[1]), g,
              Point(g.x + span[0], g.y + span[1]), h)
    because(prop_I_27, a, b, c, d, g, h)

    claim("the angle BGH is the supplement of AGH", "I.13",
          angle_at(a, g, h) + angle_at(b, g, h) == STRAIGHT)
    claim("hence the alternate angles AGH and GHD are equal", "C.N.3",
          eq_angle(a, g, h, g, h, d))
    claim("therefore AB is parallel to CD", "I.27", parallel(first, second))
    return Out()