Book XII · Proposition 4

XII.4

If there be two pyramids of the same height which have triangular bases, and each of them be divided into two pyramids equal to one another and similar to the whole, and into two equal prisms, then, as the base of the one pyramid is to the base of the other pyramid, so will all the prisms in the one pyramid be to all the prisms, being equal in multitude, in the other pyramid.Heath, 1908

The source used here misprints this enunciation — it reads “cach” where Heath has “each” ('cach' scanned for 'each'). The full errata →

Every step, checked

• the four points are not in one planegiven
• the two pyramids are of the same heightby XI.Def.9
• as the base is to the base, so are all the prisms in the one to all the prisms in the otherby XII.4

What it needs, and what needs it

Needs: XII.3

Used by: XII.5

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.13, XI.Def.9

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

What it takes on trust

• a plane is described, and XI Def. 1-2; no postulate describes a planesolid

The proposition as code

@proposition("XII.4", THEOREM, sample=samples3.polygon_base)
def prop_XII_4(a: Point3, b: Point3, c: Point3, d: Point3) -> Out:
    """Two pyramids of the same height on triangular bases, each divided as
    before: as base is to base, so are all the prisms to all the prisms."""
    hypothesis("the four points are not in one plane", not coplanar(a, b, c, d))
    first = _drawn(pyramid((a, b, c), d, "the first pyramid"))
    # A second pyramid of the same height on a wider base: the apex is carried
    # across so that it stands off the base plane by the same perpendicular.
    wider = tuple(posit3(Point3(a.x + 2 * (point.x - a.x), a.y + 2 * (point.y - a.y),
                                a.z + 2 * (point.z - a.z)), name)
                  for point, name in ((b, "P"), (c, "Q")))
    apex = posit3(Point3(d.x + (b.x - a.x), d.y + (b.y - a.y), d.z + (b.z - a.z)), "R")
    second = _drawn(pyramid((a, *wider), apex, "the second pyramid"))

    because(prop_XII_3, a, b, c, d)

    ground = plane_through(a, b, c, "the plane of the bases")
    bases = (parallelogram_area(vector_between(a, b), vector_between(a, c)) / 2,
             parallelogram_area(vector_between(a, wider[0]),
                                vector_between(a, wider[1])) / 2)
    prisms = [sum((content(piece) for piece in _divided(*corners)[2:]), Fraction(0))
              for corners in ((a, b, c, d), (a, wider[0], wider[1], apex))]

    claim("the two pyramids are of the same height", "XI.Def.9",
          on_plane(a, ground) and on_plane(wider[0], ground)
          and on_plane(wider[1], ground)
          and dot3(ground.normal(), vector_between(d, apex)) == 0)
    claim("as the base is to the base, so are all the prisms in the one to all "
          "the prisms in the other", "XII.4",
          bases[0] * prisms[1] == bases[1] * prisms[0])
    return Out(bases=bases, prisms=tuple(prisms))