Book XII · Proposition 10

XII.10

Any cone is a third part of the cylinder which has the same base with it and equal height.Heath, 1908

Every step, checked

• the axis stands at right angles to the base, so the cone is a right onegiven
• the base has a positive radius and the height is not nothinggiven
• at every stage the pyramid in the cone is a third of the prism in the cylinder, so the enclosure holds a thirdby XII.7
• and what is left over falls short of half itself at each stageby X.1
• therefore the cone is a third part of the cylinderby XII.10

What it needs, and what needs it

Needs: X.1 XII.7

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

Depth: 19 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.10", THEOREM, sample=samples3.cone_figure)
def prop_XII_10(o: Point3, a: Point3, d: Point3) -> Out:
    """Any cone is a third part of the cylinder on the same base and of the
    same height."""
    hypothesis("the axis stands at right angles to the base, so the cone is a "
               "right one", 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)
    line3(o, a, "the radius of the base")
    line3(o, d, "the axis")
    for stage in STAGES:
        _drawn(pyramid(regular_polygon(o, radius, axis, stage), d))
        _drawn(prism(regular_polygon(o, radius, axis, stage), axis))

    aside = Point3(o.x + axis[1] * (a.z - o.z) - axis[2] * (a.y - o.y),
                   o.y + axis[2] * (a.x - o.x) - axis[0] * (a.z - o.z),
                   o.z + axis[0] * (a.y - o.y) - axis[1] * (a.x - o.x))
    because(prop_XII_7, o, a, aside, d)

    found = squeeze(lambda stage: (cone_bounds(o, radius, d, stage)
                                   / cylinder_bounds(o, radius, axis, stage)),
                    Fraction(1, 3), STAGES)
    claim("at every stage the pyramid in the cone is a third of the prism in "
          "the cylinder, so the enclosure holds a third", "XII.7", found.held)
    claim("and what is left over falls short of half itself at each stage",
          "X.1", found.narrowing)
    claim("therefore the cone is a third part of the cylinder", "XII.10",
          found.held and found.narrowing)
    return Out(enclosures=found.enclosures)