Book I · Proposition 15

I.15

If two straight lines cut one another, they make the vertical angles equal to one another.Heath, 1908

Every step, checked

• the lines genuinely cross between the endpointsgiven
• angle AEC and angle CEB together are two right anglesby I.13
• angle CEB and angle BED together are two right anglesby I.13
• therefore the vertical angles AEC and BED are equalby C.N.3
• and likewise AED equals CEBby C.N.3

What it needs, and what needs it

Needs: I.13

Used by: I.16 I.29 I.44

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 figure (×2)order

The proposition as code

@proposition(
    "I.15",
    THEOREM,
    sample=samples.crossing_lines,
)
def prop_I_15(a: Point, b: Point, c: Point, d: Point) -> Out:
    crossing = posit(meet_one(line(a, b), line(c, d)), "E")
    hypothesis("the lines genuinely cross between the endpoints",
               between(a, crossing, b) and between(c, crossing, d), guard=True)

    # AC stands on the straight line AB at E, and BD on the straight line CD:
    # both are I.13's configuration, so I.13 supplies both pairs.
    because(prop_I_13, a, crossing, b, c)
    because(prop_I_13, c, crossing, d, b)

    claim("angle AEC and angle CEB together are two right angles", "I.13",
          angle_at(a, crossing, c) + angle_at(c, crossing, b) == STRAIGHT)
    claim("angle CEB and angle BED together are two right angles", "I.13",
          angle_at(c, crossing, b) + angle_at(b, crossing, d) == STRAIGHT)
    claim("therefore the vertical angles AEC and BED are equal", "C.N.3",
          eq_angle(a, crossing, c, b, crossing, d))
    claim("and likewise AED equals CEB", "C.N.3", eq_angle(a, crossing, d, c, crossing, b))
    return Out(crossing=crossing)