Book VI · Proposition 3

VI.3

If an angle of a triangle be bisected and the straight line cutting the angle cut the base also, the segments of the base will have the same ratio as the remaining sides of the triangle; and, if the segments of the base have the same ratio as the remaining sides of the triangle, the straight line joined from the vertex to the point of section will bisect the angle of the triangle.Heath, 1908

The angle bisector cuts the base in the ratio of the adjacent sides -- and the converse holds too, so the ratio identifies the bisector.

Every step, checked

• ABC is a genuine trianglegiven
• D lies on the base BCgiven
• AD bisects the angle at Aby I.9
• so the segments of the base are as the remaining sidesby VI.2
• and conversely, that ratio makes AD the bisectorby VI.2

What it needs, and what needs it

Needs: I.9 I.31 VI.2

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

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

What it takes on trust

• a circle-circle intersection is used, though no postulate asserts that two circles meet (×3)continuity
• a line-circle intersection is used, though no postulate asserts that a line meets a circle (×5)continuity

The proposition as code

@proposition(
    "VI.3",
    THEOREM,
    sample=_bisected_angle,
    note="The angle bisector cuts the base in the ratio of the adjacent sides -- "
    "and the converse holds too, so the ratio identifies the bisector.",
)
def prop_VI_3(a: Point, b: Point, c: Point, d: Point) -> Out:
    hypothesis("ABC is a genuine triangle", not collinear(a, b, c), guard=True)
    hypothesis("D lies on the base BC", on_line(d, Line.through(b, c)) and d != b and d != c)
    outline(a, b, c)
    line(a, d, "the line AD")

    because(prop_I_9, b, a, c)
    # Euclid draws CE parallel to DA to meet BA produced; then VI.2 speaks of
    # the triangle BEC, which AD cuts.
    _alongside = prop_I_31(c, a, d).parallel
    if not parallel(_alongside, Line.through(b, a)):
        _e = posit(meet_one(_alongside, Line.through(b, a)), "E")
        line(c, _e, "CE parallel to AD")
        if _e != a and _e != b:
            because(prop_VI_2, b, _e, c, a, d)

    claim("AD bisects the angle at A", "I.9", eq_angle(b, a, d, d, a, c))
    claim("so the segments of the base are as the remaining sides", "VI.2",
          length(b, d) * length(a, c) == length(d, c) * length(a, b))
    claim("and conversely, that ratio makes AD the bisector", "VI.2",
          (length(b, d) * length(a, c) == length(d, c) * length(a, b))
          == eq_angle(b, a, d, d, a, c))
    return Out(section=d)