Book XIII · Proposition 5

XIII.5

If a straight line be cut in extreme and mean ratio, and there be added to it a straight line equal to the greater segment, the whole straight line has been cut in extreme and mean ratio, and the original straight line is the greater segment.Heath, 1908

The cut reproduces itself: adding the greater segment to the whole makes a longer line cut in the same ratio, of which the old whole is now the greater segment.

Every step, checked

• A and B are distinctgiven
• AD equals the greater segment ACby Post.2
• DB is cut at A in extreme and mean ratioby VI.30
• and AB is its greater segmentby Def.3

What it needs, and what needs it

Needs: VI.30

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

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

The proposition as code

@proposition(
    "XIII.5",
    THEOREM,
    sample=samples.segment,
    note="The cut reproduces itself: adding the greater segment to the whole "
    "makes a longer line cut in the same ratio, of which the old whole is now "
    "the greater segment.",
)
def prop_XIII_5(a: Point, b: Point) -> Out:
    hypothesis("A and B are distinct", a != b)
    section = prop_VI_30(a, b).section
    added = posit(_along(a, section, -1), "D")
    line(added, b, "DB, the whole with the greater segment added to it")
    result(added)

    claim("AD equals the greater segment AC", "Post.2",
          eq_len(a, added, a, section) and between(added, a, b))
    claim("DB is cut at A in extreme and mean ratio", "VI.30",
          length(added, b) * length(added, a) == len2(a, b))
    claim("and AB is its greater segment", "Def.3", len2(a, b) > len2(added, a))
    return Out(section=section, added=added)