Book XI · Proposition 25
If a parallelepipedal solid be cut by a plane which is parallel to the opposite planes, then, as the base is to the base, so will the solid be to the solid.Heath, 1908
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.3, XI.Def.8
Depth: 12 steps of argument above the first principles. Parallel postulate: needed.
@proposition("XI.25", THEOREM, sample=samples3.corner_and_arms)
def prop_XI_25(o: Point3, a: Point3, b: Point3, c: Point3) -> Out:
"""A parallelepiped cut by a plane parallel to the opposite planes: as the
base is to the base, so is the solid to the solid."""
hypothesis("the three arms are not in one plane", not coplanar(o, a, b, c))
because(prop_XI_24, o, a, b, c)
# The cutting plane is set a third of the way along the first arm, which is
# a ratio Euclid may take at will: what the proposition asserts holds of
# every such cut, and the necessity sweep bends this one.
part = Fraction(1, 3)
cut = posit3(_along(o, a, part), "K")
over = posit3(cut + (b - o), "L")
above = posit3(cut + (c - o), "M")
nearer = _built(parallelepiped(o, cut, b, c, "the nearer solid"))
beyond = _built(parallelepiped(cut, a, over, above, "the further solid"))
cutter = plane_through(cut, over, above, "the cutting plane")
claim("the cutting plane is parallel to the two opposite planes", "XI.15",
parallel_planes(cutter, nearer.face_plane(4))
and parallel_planes(cutter, beyond.face_plane(5)))
here, there = _base_area(o, cut, b), _base_area(cut, a, over)
claim("as the base is to the base, so is the solid to the solid", "XI.25",
here * content(beyond) == there * content(nearer))
return Out(nearer=nearer, beyond=beyond, cut=cut, bases=(here, there))