Book XI · Proposition 36

XI.36

If three straight lines be proportional, the parallelepipedal solid formed out of the three is equal to the parallelepipedal solid on the mean which is equilateral, but equiangular with the aforesaid solid.Heath, 1908

Every step, checked

What it needs, and what needs it

Needs: XI.34

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, XI.Def.10, XI.Def.3, XI.Def.8, XI.Def.9

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

What it takes on trust

Nothing. It draws no intersections and reads nothing off the picture.

The proposition as code

@proposition("XI.36", THEOREM, sample=samples3.corner_and_arms)
def prop_XI_36(o: Point3, a: Point3, b: Point3, c: Point3) -> Out:
    """If three straight lines be proportional, the parallelepiped on them is
    equal to the equilateral one on the mean which is equiangular with it."""
    hypothesis("the three arms are not in one plane", not coplanar(o, a, b, c))
    ratio = Fraction(3, 2)
    # Three lines in proportion, taken as one length, that length by the ratio,
    # and by the ratio again: the mean is the square root of the extremes'
    # rectangle exactly, and every one of the three stays rational.
    lines = (Fraction(1), ratio, ratio * ratio)
    hypothesis("the three straight lines are proportional",
               lines[1] * lines[1] == lines[0] * lines[2])

    directions = tuple(unit(vector_between(o, point)) for point in (a, b, c))
    unequal = _built(parallelepiped(
        o, *[posit3(_arm_at(o, step, reach), name)
             for step, reach, name in zip(directions, lines, ("P", "Q", "R"))],
        "the solid on the three lines"))
    square = _built(parallelepiped(
        o, *[_arm_at(o, step, lines[1]) for step in directions],
        "the equilateral solid on the mean"))

    because(prop_XI_34, o, a, b, c)

    claim("the second solid is equilateral", "XI.Def.9",
          len2(o, square.vertices[1]) == len2(o, square.vertices[3])
          == len2(o, square.vertices[4]))
    claim("and it is equiangular with the first", "XI.Def.9",
          _solid_angle_of(o, tuple(square.vertices[index] for index in (1, 3, 4)))
          == _solid_angle_of(o, tuple(unequal.vertices[index] for index in (1, 3, 4))))
    claim("therefore the two solids are equal", "XI.36",
          content(unequal) == content(square))
    return Out(solids=(unequal, square), lines=lines)