Book XII · Proposition 5

XII.5

Pyramids which are of the same height and have triangular bases are to one another as the bases.Heath, 1908

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 is the pyramid to the pyramidby XII.5

What it needs, and what needs it

Needs: XII.4

Used by: XII.6 XII.7 XII.9

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: 17 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.5", THEOREM, sample=samples3.polygon_base)
def prop_XII_5(a: Point3, b: Point3, c: Point3, d: Point3) -> Out:
    """Pyramids of the same height on triangular bases are to one another as
    their bases."""
    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"))
    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_4, 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)
    claim("the two pyramids are of the same height", "XI.Def.9",
          dot3(ground.normal(), vector_between(d, apex)) == 0)
    claim("as the base is to the base, so is the pyramid to the pyramid",
          "XII.5", bases[0] * content(second) == bases[1] * content(first))
    return Out(pyramids=(first, second), bases=bases)