Book I · Proposition 9

I.9

To bisect a given rectilineal angle.Heath, 1908

Every step, checked

• BD = BE by constructionby I.3
• DF = EF, sides of the equilateral triangle DEFby I.1
• triangles BDF and BEF have three sides equalby I.8
• therefore angle ABF = angle FBC: the angle is bisectedby I.8

What it needs, and what needs it

Needs: I.1 I.3 I.8

Used by: I.10 IV.4 VI.3

Rests on: C.N.1, C.N.3, C.N.4, C.N.5, 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.9",
    CONSTRUCTION,
    sample=samples.angle_config,
)
def prop_I_9(a: Point, b: Point, c: Point) -> Out:
    """Cut equal lengths along the two rays, then hang an equilateral triangle
    between their ends; the line to its apex bisects the angle."""
    # D is taken at random on BA and BE cut off equal to it, which is I.3's
    # business. A quarter of the shorter arm keeps BD strictly inside BC, the
    # "greater" that I.3 asks for.
    reach = min(len2(b, a), len2(b, c)) / 4
    gauge = circle_with_radius2(b, reach, "circle centre B")
    d = posit(meet(line(b, a), gauge)[1], "D")
    e = posit(prop_I_3(b, c, d, b).cut, "E")

    apex = posit(prop_I_1(d, e).apex, "F")
    if apex == b:
        # the equilateral apex landed on the vertex itself (a 60-degree angle);
        # the triangle on the other side of DE serves just as well
        apex = posit(meet(circle(d, e), circle(e, d))[1], "F")
    bisector = line(b, apex, "the bisector BF")

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

    claim("BD = BE by construction", "I.3", eq_len(b, d, b, e))
    claim("DF = EF, sides of the equilateral triangle DEF", "I.1", eq_len(d, apex, e, apex))
    claim("triangles BDF and BEF have three sides equal", "I.8", congruent_sss((b, d, apex), (b, e, apex)))
    claim("therefore angle ABF = angle FBC: the angle is bisected", "I.8",
          eq_angle(a, b, apex, apex, b, c))
    return Out(bisector=bisector, through=apex)