TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-28

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.

Cauchy's mean value theorem: for $f, g$ continuous on $[a, b]$ with $a < b$ and differentiable on $(a, b)$ there is $c \in (a, b)$ with $(f (b) - f (a)) g^{'} (c) = (g (b) - g (a)) f^{'} (c)$ ; no hypothesis on $g^{'}$ is needed in this product form

Statement

Let $a, b \in R$ with $a < b$ and let $f, g : [a, b] \to R$ be continuous on $[a, b]$ (Continuity of $f : A \to R$ at a point of $A$ and on $A$ : the $ε$ - $δ$ condition, its agreement with $\lim_{x \to c} f (x) = f (c)$ at a limit point, and continuity at an isolated point, Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length) and differentiable at every point of $(a, b)$ as functions on $[a, b]$ (The derivative $f^{'} (c) = \lim_{x \to c} \frac{f (x) - f (c)}{x - c}$ of $f : A \to R$ at a point $c \in A$ that is a limit point of $A$ , and differentiability on a set). Then there is $c \in (a, b)$ with

$(f (b) - f (a)) g^{'} (c) = (g (b) - g (a)) f^{'} (c) .$

The statement is a product identity, and that is deliberate. The familiar quotient form

$\frac{f (b) - f (a)}{g (b) - g (a)} = \frac{f^{'} (c)}{g^{'} (c)}$

is not asserted here, and it is not equivalent: its left side needs $g (b) \neq g (a)$ and its right side needs $g^{'} (c) \neq 0$ , and neither follows from the hypotheses. The product form above needs neither, holds under exactly the hypotheses stated, and specialises to the quotient form whenever both denominators happen to be nonzero. The companion page exhibits an $f$ and a $g$ for which the quotient form is meaningless while the product form holds.

Facts & Assumptions

Given: Reals $a < b$ and functions $f, g : [a, b] \to R$ , both continuous on $[a, b]$ and both differentiable at every point of $(a, b)$ .

[L1]

Rolle's theorem (Rolle's theorem: if $a < b$ , $f$ is continuous on $[a, b]$ , differentiable at every point of $(a, b)$ , and $f (a) = f (b)$ , then $f^{'} (c) = 0$ for some $c \in (a, b)$ ): a function continuous on $[a, b]$ , differentiable at every point of $(a, b)$ and taking equal values at $a$ and at $b$ has a vanishing derivative at some point of $(a, b)$ .

[L2]

Algebra of continuous functions (Sums, scalar multiples, products, absolute values, maxima, minima and quotients with nonvanishing denominator of continuous functions are continuous, as are constants, the identity and every polynomial function, claim 1): sums and scalar multiples of functions continuous on a set are continuous on that set.

[L3]

Algebra of derivatives (Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ , claims 1 and 2): at a limit point of the common domain, a sum of functions differentiable there is differentiable with the sum of the derivatives, and a scalar multiple with the scalar multiple of the derivative.

[L4]

Every point of $(a, b)$ lies in $[a, b]$ and is a limit point of $[a, b]$ , since $[a, b]$ is order-convex with at least two elements when $a < b$ (The derivative $f^{'} (c) = \lim_{x \to c} \frac{f (x) - f (c)}{x - c}$ of $f : A \to R$ at a point $c \in A$ that is a limit point of $A$ , and differentiability on a set, Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length).

Proof

technique · direct

1.1

Put $λ : = f (b) - f (a)$ and $μ : = g (b) - g (a)$ , two reals, and define $h : [a, b] \to R$ by $h (x) : = λ g (x) - μ f (x)$ .

construct

2.1

$h$ is continuous on $[a, b]$ , being the sum of the scalar multiples $λ g$ and $(- μ) f$ of two functions continuous on $[a, b]$ .

step 1.1L2

2.2

$h$ is differentiable at every $c \in (a, b)$ with $h^{'} (c) = λ g^{'} (c) - μ f^{'} (c)$ : such a $c$ is a limit point of $[a, b]$ by [L4], and $f$ and $g$ are differentiable there, so the scalar-multiple and sum rules of [L3] apply on the domain $[a, b]$ .

step 1.1L3L4

2.3

$h (a) = h (b)$ . Expanding, $h (a) = (f (b) - f (a)) g (a) - (g (b) - g (a)) f (a) = f (b) g (a) - f (a) g (a) - g (b) f (a) + g (a) f (a) = f (b) g (a) - g (b) f (a)$ , and $h (b) = (f (b) - f (a)) g (b) - (g (b) - g (a)) f (b) = f (b) g (b) - f (a) g (b) - g (b) f (b) + g (a) f (b) = g (a) f (b) - f (a) g (b)$ . The two expressions are the same.

step 1.1algebra

3.1

By steps 2.1, 2.2 and 2.3 the function $h$ satisfies every hypothesis of [L1], so there is $c \in (a, b)$ with $h^{'} (c) = 0$ , that is $λ g^{'} (c) - μ f^{'} (c) = 0$ , that is $(f (b) - f (a)) g^{'} (c) = (g (b) - g (a)) f^{'} (c)$ .

step 2.1step 2.2step 2.3L1∎

Remarks

Where the auxiliary function comes from. $h$ is built so that the two cross terms $f (a) g (a)$ and $f (b) g (b)$ cancel against themselves at the two endpoints, leaving the same antisymmetric expression $f (b) g (a) - f (a) g (b)$ at each. Nothing is optimised and nothing is guessed: the two coefficients are forced, up to a common scalar, by the requirement $h (a) = h (b)$ .
The ordinary mean value theorem is the case $g (x) = x$ , and it is recorded as the next item rather than reproved. Cauchy's theorem is the more general statement and is proved first for that reason, not because it is harder: it costs one application of Rolle either way.
What fails in the quotient form. If $g (a) = g (b)$ the left side is not a real number at all, and the theorem still says something: it says $(f (b) - f (a)) g^{'} (c) = 0$ for some $c \in (a, b)$ . That is the case worked out in With $f (x) = x^{3}$ and $g (x) = x^{2}$ on $[- 1, 1]$ the quotient form $\frac{f (b) - f (a)}{g (b) - g (a)} = \frac{f^{'} (c)}{g^{'} (c)}$ is meaningless because $g (b) = g (a)$ , while the product form of Cauchy's theorem still holds ↗.

Depends on

Used by

Dependency tree · two levels

33 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

Mean value theorem (Wikipedia) (standard reference, not scraped)
W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 5 (Thm 5.9) (standard reference, not scraped)
J. Lebl, Basic Analysis I, §4.2 (standard reference, not scraped)
J. Hunter, An Introduction to Real Analysis (standard reference, not scraped)

Cauchy's mean value theorem: for f,gf,g continuous on [a,b][a,b] with a<ba<b and differentiable on (a,b)(a,b) there is c∈(a,b)c∈(a,b) with (f(b)−f(a))g′(c)=(g(b)−g(a))f′(c)(f(b)−f(a))g′(c)=(g(b)−g(a))f′(c); no hypothesis on g′g′ is needed in this product form