Book I · Proposition 31

I.31

Through a given point to draw a straight line parallel to a given straight line.Heath, 1908

Every step, checked

• A does not lie on BCgiven
• the angle EAD equals the angle ADC, and they are alternateby I.23
• therefore EF is parallel to BCby I.27

What it needs, and what needs it

Needs: I.23 I.27

Used by: I.32 I.38 I.39 I.40 I.42 I.43 I.44 I.47 VI.3 VI.9 VI.10 VI.11 VI.12

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

• a circle-circle intersection is used, though no postulate asserts that two circles meetcontinuity
• a line-circle intersection is used, though no postulate asserts that a line meets a circlecontinuity

The proposition as code

@proposition(
    "I.31",
    CONSTRUCTION,
    sample=samples.line_and_external_point,
)
def prop_I_31(a: Point, b: Point, c: Point) -> Out:
    """Through A, parallel to BC.  Euclid copies the angle ADC over to A on the
    far side of AD, and I.27 does the rest."""
    given = line(b, c, "the given line BC")
    hypothesis("A does not lie on BC", not on_line(a, given))

    joined = line(a, b, "join AD")
    copied = prop_I_23(a, b, c, a, b, apart_from=c)
    e = posit(copied.ray_through, "E")
    drawn = line(a, e, "the parallel EF")

    # AD crosses EF at A and BC at B, at an end of each, so both are named by
    # points straddling the crossing before I.27 is asked for the parallel.
    prop_I_27(e, Point(2 * a.x - e.x, 2 * a.y - e.y),
              Point(2 * b.x - c.x, 2 * b.y - c.y), c, a, b)

    claim("the angle EAD equals the angle ADC, and they are alternate", "I.23",
          eq_angle(e, a, b, a, b, c))
    claim("therefore EF is parallel to BC", "I.27", parallel(drawn, given))
    return Out(parallel=drawn, through=e)