Book VI · Proposition 11

VI.11

To two given straight lines to find a third proportional.Heath, 1908

Every step, checked

• A and B are distinctgiven
• the second line is a genuine magnitudegiven
• CF is parallel to BEby I.31
• so AB is to AC as AC is to AFby VI.2

What it needs, and what needs it

Needs: I.31 VI.2

Used by: VI.19

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 meetcontinuity
• a line-circle intersection is used, though no postulate asserts that a line meets a circlecontinuity
• the 'on_line' fact (occurrence 1) is true in some configurations and false in otherscase

The proposition as code

@proposition(
    "VI.11",
    CONSTRUCTION,
    sample=lambda rng: samples.segment(rng) + (Fraction(rng.randint(2, 7), 4),),
)
def prop_VI_11(a: Point, b: Point, ratio) -> Out:
    """To AB and AC, find the third proportional: AB : AC = AC : x."""
    hypothesis("A and B are distinct", a != b)
    hypothesis("the second line is a genuine magnitude", sign(ratio) > 0, guard=True)
    line(a, b, "the first given line AB")
    c = posit(_along(a, b, ratio), "C")

    aside = posit(Point(a.x + (b.y - a.y), a.y - (b.x - a.x)), "D")
    line(a, aside, "a line through A")
    e = posit(_along(a, aside, ratio), "E")
    line(b, e, "the join BE")
    third = posit(_along(a, aside, ratio * ratio), "F")
    line(c, third, "the parallel through C")

    # A ratio of 1 puts C on B and F on E, and there is then no triangle for
    # either appeal to be about: the parallel through C is the join BE itself.
    _proper = not collinear(a, b, e) and not on_line(c, Line.through(b, e))
    if _proper:
        because(prop_I_31, c, b, e)
        # ABE is the triangle, C on AB and F on AE, and CF is the parallel:
        # that is VI.2's figure exactly.
        because(prop_VI_2, a, b, e, c, third)

    claim("CF is parallel to BE", "I.31",
          parallel(Line.through(c, third), Line.through(b, e)))
    claim("so AB is to AC as AC is to AF", "VI.2",
          length(a, b) * length(a, third) == length(a, c) * length(a, c))
    return Out(third=third)