Book XII · Proposition 3

XII.3

Any pyramid which has a triangular base is divided into two pyramids equal and similar to one another, similar to the whole and having triangular bases, and into two equal prisms; and the two prisms are greater than the half of the whole pyramid.Heath, 1908

Every step, checked

• the four points are not in one planegiven
• the two pyramids are equal to one another and similar to the whole, every edge of each being half the edge it answers toby XI.Def.9
• the pieces together make the whole pyramidby XII.3
• the two prisms are equal to one anotherby XI.39
• and the two prisms together are greater than the half of the whole pyramidby XII.3

What it needs, and what needs it

Needs: XI.39

Used by: XII.4

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: 15 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("XII.3", THEOREM, sample=samples3.polygon_base)
def prop_XII_3(a: Point3, b: Point3, c: Point3, d: Point3) -> Out:
    """A pyramid on a triangular base divides into two pyramids similar to the
    whole and two equal prisms, and the prisms are greater than half of it."""
    hypothesis("the four points are not in one plane", not coplanar(a, b, c, d))
    whole = _drawn(pyramid((a, b, c), d, "the pyramid"))
    first, second, one_prism, other_prism = _divided(a, b, c, d)
    for piece in (first, second, one_prism, other_prism):
        _drawn(piece)

    held = content(whole)
    e, f, g, h, k, ell = _bisections(a, b, c, d)
    claim("the two pyramids are equal to one another and similar to the whole, "
          "every edge of each being half the edge it answers to", "XI.Def.9",
          content(first) == content(second)
          and all(4 * len2(near, far) == len2(one, other) for near, far, one, other in
                  ((e, g, b, c), (g, h, c, d), (e, h, b, d),
                   (h, k, a, b), (k, ell, b, c), (h, ell, a, c))))
    claim("the pieces together make the whole pyramid", "XII.3",
          content(first) + content(second) + content(one_prism)
          + content(other_prism) == held)
    claim("the two prisms are equal to one another", "XI.39",
          content(one_prism) == content(other_prism))
    claim("and the two prisms together are greater than the half of the whole "
          "pyramid", "XII.3",
          sign(2 * (content(one_prism) + content(other_prism)) - held) > 0)
    return Out(pyramids=(first, second), prisms=(one_prism, other_prism),
               whole=whole)