Book VI · Proposition 9

VI.9

From a given straight line to cut off a prescribed part.Heath, 1908

Every step, checked

• A and B are distinctgiven
• a genuine part is asked forgiven
• the divisions of the second line are equalby I.3
• the line through the first division is parallel to CBby I.31
• so AD is the part asked forby VI.2

What it needs, and what needs it

Needs: I.3 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 (×2)continuity
• a line-circle intersection is used, though no postulate asserts that a line meets a circle (×4)continuity
• the proof evaluates a different number of facts on different configurations (seen: [2, 3, 4, 5, 6]), so it is following more than one route through the diagramcase

The proposition as code

@proposition(
    "VI.9",
    CONSTRUCTION,
    sample=lambda rng: samples.segment(rng) + (rng.randint(2, 6),),
)
def prop_VI_9(a: Point, b: Point, parts: int) -> Out:
    """Cut off from AB the prescribed part -- one of `parts` equal pieces."""
    hypothesis("A and B are distinct", a != b)
    hypothesis("a genuine part is asked for", parts >= 2, guard=True)
    line(a, b, "the given line AB")

    # Euclid lays off equal lengths on a second line through A and joins the
    # last to B; the parallels through the divisions cut AB proportionally.
    aside = posit(Point(a.x + (b.y - a.y), a.y - (b.x - a.x)), "C")
    marks = [posit(_along(a, aside, Fraction(k, parts)), f"M{k}") for k in range(1, parts + 1)]
    line(a, aside, "the line laid off from A")
    line(marks[-1], b, "the join CB")
    cut = posit(_along(a, b, Fraction(1, parts)), "D")
    line(marks[0], cut, "the parallel through the first division")

    # The lesser line is named from its far end: I.3 places it at A through
    # I.2, and I.2 joins the point to an end of the line.
    because(prop_I_3, a, aside, marks[0], a)
    because(prop_I_31, marks[0], marks[-1], b)
    because(prop_VI_2, a, marks[-1], b, marks[0], cut)

    claim("the divisions of the second line are equal", "I.3",
          all(eq_len(marks[k], marks[k + 1], a, marks[0]) for k in range(len(marks) - 1)))
    claim("the line through the first division is parallel to CB", "I.31",
          parallel(Line.through(marks[0], cut), Line.through(marks[-1], b)))
    claim("so AD is the part asked for", "VI.2", parts * length(a, cut) == length(a, b))
    return Out(part=cut)