Book I · Proposition 11

I.11

To draw a straight line at right angles to a given straight line from a given point on it.Heath, 1908

Every step, checked

• C lies on ABgiven
• C is not an endpointgiven
• CD = CE by constructionby I.3
• FD = FE, sides of the equilateral triangleby I.1
• triangles DCF and ECF have three sides equalby I.8
• so the adjacent angles are equal, and each is rightby Def.10
• CF is at right angles to ABby Def.10

What it needs, and what needs it

Needs: I.1 I.3 I.8

Used by: I.46 I.48 II.9 II.10 II.14 III.1 III.9 IV.5 IV.6 VI.13

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

Depth: 6 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 meet (×2)continuity
• a line-circle intersection is used, though no postulate asserts that a line meets a circle (×4)continuity

The proposition as code

@proposition(
    "I.11",
    CONSTRUCTION,
    sample=samples.point_on_segment,
)
def prop_I_11(a: Point, b: Point, c: Point) -> Out:
    hypothesis("C lies on AB", on_line(c, Line.through(a, b)))
    hypothesis("C is not an endpoint", c != a and c != b)

    reach = min(len2(c, a), len2(c, b)) / 4
    gauge = circle_with_radius2(c, reach, "circle centre C")
    d = posit(meet(line(a, b), gauge)[0], "D")
    e = posit(prop_I_3(c, b, d, c).cut, "E")
    apex = posit(prop_I_1(d, e).apex, "F")
    upright = line(c, apex, "the perpendicular CF")

    because(prop_I_8, d, c, apex, e, c, apex)

    claim("CD = CE by construction", "I.3", eq_len(c, d, c, e))
    claim("FD = FE, sides of the equilateral triangle", "I.1", eq_len(apex, d, apex, e))
    claim("triangles DCF and ECF have three sides equal", "I.8",
          congruent_sss((d, c, apex), (e, c, apex)))
    claim("so the adjacent angles are equal, and each is right", "Def.10",
          right_angle(a, c, apex))
    claim("CF is at right angles to AB", "Def.10", perpendicular(upright, Line.through(a, b)))
    return Out(perpendicular=upright, through=apex)