CorollaryStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-24

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The washer formula for a solid of revolution between two nonnegative profiles

Statement

Let $a \leq b$ and let $f, g : [a, b] \to [0, \infty)$ be continuous with $g \leq f$ . Revolve the region $g (x) \leq y \leq f (x)$ about the $x$ -axis. The resulting washer solid is compact and Jordan measurable. Its volume is $π \int_{a}^{b} (f (x)^{2} - g (x)^{2}) d x$ .

The same assertion holds about any coordinate axis after the corresponding coordinate permutation.

Facts & Assumptions

Given: The profiles $0 \leq g \leq f$ and the washer solid $W : = {(x, y, z) : a \leq x \leq b, g (x)^{2} \leq y^{2} + z^{2} \leq f (x)^{2}}$ .

[F1]

The disc solid of a continuous nonnegative profile is compact and Jordan measurable (The disc formula for the volume of a solid of revolution).

[F2]

A closed disc of radius $r \geq 0$ has Jordan content $π r^{2}$ (A closed disc of radius $r \geq 0$ has Jordan content $π r^{2}$ ).

[F3]

Jordan content is additive when two bounded Jordan sets meet in a content-zero set (Jordan content is finitely additive when the overlap has content zero).

[F4]

A bounded set is Jordan measurable if and only if its boundary has content zero (A bounded set in $R^{m}$ is Jordan measurable iff its boundary is null, equivalently of content zero).

[F5]

If a bounded Jordan set has Jordan-measurable sections outside a content-zero parameter set, then its completed sectional-content function is integrable and its integral is the set's content (Cavalieri: Jordan content is the integral of sectional contents, and equal sections give equal content).

[F6]

A linear coordinate permutation preserves Jordan measurability and content because its determinant has absolute value $1$ (A linear endomorphism of $R^{n}$ sends bounded Jordan sets to bounded Jordan sets and scales their content by the absolute determinant).

Proof

technique · direct

1.1

The outer disc solid and the inner disc solid are compact Jordan sets by [F1]. The boundary of $W$ , the outer solid with the interior of the inner solid removed, lies in the union of their content-zero boundaries; hence [F4] makes $W$ compact and Jordan measurable.

givenF1F4

2.1

At coordinate $x$ , the section is the annulus between radii $g (x)$ and $f (x)$ . Splitting the outer disc into that annulus and the inner disc, whose overlap is a boundary circle of content zero, [F2] and [F3] give section content $π (f (x)^{2} - g (x)^{2})$ .

step 1.1F2F3algebra

3.1

By [F5], integration of the continuous section-content function gives the displayed washer formula. It gives zero when $f = g$ and reduces to the disc formula when $g = 0$ . By [F6], coordinate permutations preserve the construction and volume, proving the coordinate-axis clause.

step 2.1F5F6∎

Depends on

Used by

Dependency tree · two levels

36 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Sigurd Angenent, Math 221 lecture notes, Chapter 8 §4 (standard reference, not scraped)