Book I · Proposition 14

I.14

If with any straight line, and at a point on it, two straight lines not lying on the same side make the adjacent angles equal to two right angles, the two straight lines will be in a straight line with one another.Heath, 1908

Every step, checked

• D is off the line and A, C lie on opposite sides of Bgiven
• the adjacent angles sum to two right anglesgiven
• with BE in a straight line with AB, the angles ABD and DBE are two right anglesby I.13
• so the angle DBE equals the angle DBC, and BE falls along BCby C.N.3
• BA and BC are therefore in one straight lineby I.13

What it needs, and what needs it

Needs: I.13

Used by: VI.32

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

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

What it takes on trust

• the argument reads a 'between' fact off the figureorder

The proposition as code

@proposition(
    "I.14",
    THEOREM,
    sample=samples.straight_line_with_ray,
)
def prop_I_14(a: Point, b: Point, c: Point, d: Point) -> Out:
    hypothesis("D is off the line and A, C lie on opposite sides of B",
               not collinear(a, b, d) and between(a, b, c))
    outline(a, b, c, close=False)
    line(b, d)
    total = angle_at(a, b, d) + angle_at(d, b, c)
    hypothesis("the adjacent angles sum to two right angles", total == STRAIGHT)

    # Euclid supposes BE, and not BC, to be in a straight line with AB, and
    # reaches an absurdity. The supposed line is drawable even though the
    # absurdity is not, so I.13 is applied to it and the two angles compared.
    supposed = posit(Point(b.x + (b.x - a.x), b.y + (b.y - a.y)), "E")
    straight_on = prop_I_13(a, b, supposed, d).angles

    claim("with BE in a straight line with AB, the angles ABD and DBE are two "
          "right angles", "I.13", straight_on[0] + straight_on[1] == STRAIGHT)
    claim("so the angle DBE equals the angle DBC, and BE falls along BC",
          "C.N.3", angle_at(d, b, supposed) == angle_at(d, b, c))
    claim("BA and BC are therefore in one straight line", "I.13", collinear(a, b, c))
    return Out(supposed=supposed)