Book XII · Proposition 15
In equal cones and cylinders the bases are reciprocally proportional to the heights; and those cones and cylinders in which the bases are reciprocally proportional to the heights are equal.Heath, 1908
Rests on: VI.Def.1, XI.Def.3, XI.Def.8
Depth: 5 steps of argument above the first principles. Parallel postulate: not needed.
Nothing. It draws no intersections and reads nothing off the picture.
@proposition("XII.15", THEOREM, sample=samples3.cone_figure)
def prop_XII_15(o: Point3, a: Point3, d: Point3) -> Out:
"""In equal cones and cylinders the bases are reciprocally proportional to
the heights, and conversely."""
hypothesis("the axis stands at right angles to the base",
dot3(vector_between(o, a), vector_between(o, d)) == 0)
hypothesis("the base has a positive radius and the height is not nothing",
o != a and o != d)
radius, axis = _cone_figure(o, a, d)
# The base doubled in area is the radius taken in the ratio of the side of
# the square on two, and the height halved answers it: so the two cylinders
# are equal, and reciprocally proportional is what they are.
spread = sqrt(Fraction(2))
centre = posit3(Point3(o.x + 9 * (a.x - o.x), o.y + 9 * (a.y - o.y),
o.z + 9 * (a.z - o.z)), "P")
lower = tuple(component / 2 for component in axis)
top = posit3(Point3(centre.x + lower[0], centre.y + lower[1],
centre.z + lower[2]), "Q")
line3(o, d, "the first axis")
line3(centre, top, "the second axis")
for stage in STAGES:
_ring(regular_polygon(o, radius, axis, stage))
_ring(regular_polygon(centre, spread * radius, axis, stage))
because(prop_XII_14, o, a, d)
bases = (len2(o, a), 2 * len2(o, a))
heights = (length3(o, d), length3(o, d) / 2)
found = squeeze(lambda stage: (cylinder_bounds(o, radius, axis, stage)
/ cylinder_bounds(centre, spread * radius,
lower, stage)),
Fraction(1), STAGES)
claim("the bases are reciprocally proportional to the heights", "XII.15",
bases[0] * heights[0] == bases[1] * heights[1])
claim("the enclosure of the ratio of the two cylinders holds unity at every "
"stage, so they are equal", "XII.14", found.held)
claim("and what is left over falls short of half itself at each stage",
"X.1", found.narrowing)
claim("therefore equal cones and cylinders have their bases reciprocally "
"proportional to their heights, and conversely", "XII.15",
found.held and found.narrowing)
return Out(enclosures=found.enclosures, bases=bases, heights=heights)