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 surface generated by rotating on has area
Example
Rotate the graph , , about the -axis. The resulting surface has area
The profile is positive in the parameter interior and vanishes only at its endpoints, where the generating curve meets the axis of revolution.
Facts & Assumptions
Given: The radius function on and the surface obtained by rotating its graph about the -axis.
Under the hypotheses of the scalar surface-integral theorem for a surface of revolution, the rotated surface has area (The surface of revolution has area ).
Those hypotheses require and to be on a neighbourhood of , positive on , and allowed to vanish only at the endpoints (Scalar surface integrals on a surface of revolution).
, and for every with ; thus is the first positive zero of sine, in particular (Pi is the first positive zero of sine).
The functions and are differentiable on , with and ; also and (The derivatives of sine and cosine are cosine and minus sine).
For a real-valued function on , differentiability at a limit point implies continuity there (A function differentiable at is continuous at ).
The function is odd, strictly increasing, and onto; is positive; ; and (Addition formulas, identities, parity, and derivatives of the hyperbolic functions).
Let be order-convex with at least two elements, let be continuous and injective, and let be its inverse. If is differentiable at with , then is differentiable at and (Derivative of an inverse: if is continuous and injective on a nondegenerate interval and differentiable at with , then the inverse is differentiable at with ; and if then is not differentiable at ).
For every real , is continuous and differentiable on , with derivative (Continuity and derivatives of positive-base real powers).
If and , then the real power agrees with the rational power; in particular this holds for (The exponential definition of real powers agrees with the existing rational powers).
Every nonnegative real has a unique nonnegative square root (Square roots exist: a unique with ; the positives are ).
If real functions and are differentiable at the relevant points, then (The chain rule, in one line from Carathéodory: if is differentiable at and is differentiable at , then is differentiable at with ).
Products, sums, and scalar multiples obey their usual derivative rules (Sums, scalar multiples, products and quotients: , , , and when ).
Every continuous real-valued function on a nondegenerate closed interval is Riemann integrable there (A continuous function on is Riemann integrable, by Heine-Cantor and Riemann's criterion).
If , is differentiable at every point of , and is integrable, then (The second fundamental theorem: if is differentiable on with and is integrable, then ).
Verification
Facts [L1], [L2], and [L3] verify the hypotheses in [F2], so [F1] gives .
Let and . Facts [L3], [L4], and [L5] give , where positivity of and uniqueness in [L9] select the nonnegative square root. Since is an odd bijection, its inverse is odd, so .
Since by [L1], the interval is nondegenerate. The function is continuous on this interval and hence integrable there.
Define . Using step 1.2, the derivative of the positive square root, and the chain and product rules gives .
By the fundamental theorem, step 1.3, and step 2.1, the integral in step 1.1 is : fact [L14] gives the cosine endpoint values, and the oddness in step 1.2 changes to . Fact [L6] also gives .
Substituting step 3.1 into the area formula of step 1.1 gives .
Remarks
The endpoint zeros satisfy the source theorem's boundary allowance. The integrand stays continuous there, since its square-root factor is at least , so no improper-integral convention enters the calculation.
Depends on
- The surface of revolution has area $2\pi\int_a^b r(s)\sqrt{1+r'(s)^2}\,ds$
- Scalar surface integrals on a surface of revolution
- Pi is the first positive zero of sine
- The derivatives of sine and cosine are cosine and minus sine
- A function differentiable at $c$ is continuous at $c$
- Quarter-turn values and shifts by pi/2 and pi
- Addition formulas, identities, parity, and derivatives of the hyperbolic functions
- Derivative of an inverse: if $f$ is continuous and injective on a nondegenerate interval $I$ and differentiable at $c \in I$ with $f'(c) \ne 0$, then the inverse $g$ is differentiable at $f(c)$ with $g'(f(c)) = 1/f'(c)$; and if $f'(c) = 0$ then $g$ is not differentiable at $f(c)$
- Logarithm formulas for inverse sinh, inverse cosh, and inverse tanh on their natural domains
- Continuity and derivatives of positive-base real powers
- The exponential definition of real powers agrees with the existing rational powers
- Square roots exist: a unique $\sqrt{a} \ge 0$ with $(\sqrt{a})^2 = a$; the positives are $\{x^2 : x \neq 0\}$
- The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g(c)$, then $f \circ g$ is differentiable at $c$ with $(f \circ g)'(c) = f'(g(c))\,g'(c)$
- Sums, scalar multiples, products and quotients: $(f+g)'(c) = f'(c) + g'(c)$, $(\alpha f)'(c) = \alpha f'(c)$, $(fg)'(c) = f'(c)g(c) + f(c)g'(c)$, and $(f/g)'(c) = \bigl(f'(c)g(c) - f(c)g'(c)\bigr)/g(c)^{2}$ when $g(c) \ne 0$
- A continuous function on $[a,b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion
- The second fundamental theorem: if $G$ is differentiable on $[a,b]$ with $G' = f$ and $f$ is integrable, then $\int_a^b f = G(b)-G(a)$
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
80 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
- OpenStax, Calculus Volume 2, section 2.4 Arc Length of a Curve and Surface Area (standard reference, not scraped)
- APEX Calculus II, Version 2.0, section 7.4, Example 214 (standard reference, not scraped)