Book I · Proposition 10

I.10

To bisect a given finite straight line.Heath, 1908

Every step, checked

• AD = DB: the line is bisectedby I.4
• D lies on ABby Def.4
• D lies between A and Bby C.N.5

What it needs, and what needs it

Needs: I.1 I.4 I.9

Used by: I.12 I.16 I.42 II.5 II.6 II.9 II.10 II.11 II.14 III.1 III.2 III.3 III.9 III.14 III.15 III.30 III.33 III.35 III.36 IV.5 IV.8 IV.9 IV.13 IV.16 VI.13 VI.27 VI.28 VI.29 XIII.1 XIII.3

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

Depth: 7 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 (×4)continuity
• a line-circle intersection is used, though no postulate asserts that a line meets a circle (×4)continuity
• the argument reads a 'between' fact off the figureorder

The proposition as code

@proposition(
    "I.10",
    CONSTRUCTION,
    sample=samples.segment,
)
def prop_I_10(a: Point, b: Point) -> Out:
    apex = posit(prop_I_1(a, b).apex, "C")
    bisected = prop_I_9(a, apex, b)
    middle = posit(meet_one(bisected.bisector, line(a, b)), "D")

    # AC and BC are sides of the equilateral triangle, CD is common, and the
    # angles at C were bisected: that is I.4's own hypothesis, so I.4 concludes.
    because(prop_I_4, apex, a, middle, apex, b, middle)
    claim("AD = DB: the line is bisected", "I.4", eq_len(a, middle, middle, b))
    claim("D lies on AB", "Def.4", on_line(middle, Line.through(a, b)))
    claim("D lies between A and B", "C.N.5", between(a, middle, b))
    return Out(midpoint=middle)