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.

✓ 16 results · all verified · 15 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 1 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

The Derivative and the Mean Value Theorems

1 · Prerequisites

2 · Summary

Objective. This page defines the derivative of a real function at a point, proves the rules that make it computable, and then proves four central theorems whose hypotheses use differentiability: Fermat's interior extremum theorem, Rolle's theorem, Cauchy's mean value theorem, and the mean value theorem itself. It closes with what the mean value theorem is actually spent on downstream: a vanishing derivative forces a constant, the sign of the derivative controls monotonicity, and a bound on the derivative gives a Lipschitz bound on the function.

The definition, and the two obligations it carries. 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 takes $f : A \to R$ and a point $c \in A$ that is also a limit point of $A$ , forms the difference quotient $q (x) = (f (x) - f (c)) / (x - c)$ on $A ∖ {c}$ , and defines $f^{'} (c)$ to be its limit at $c$ when that exists. Both obligations are discharged in the definition itself rather than assumed. The point must be a limit point of $A$ , since otherwise The $ε$ - $δ$ limit $\lim_{x \to c} f (x) = L$ of $f : A \to R$ at a limit point $c$ of $A$ leaves the symbol undefined and every real would satisfy the $ε$ - $δ$ condition vacuously; and the limit is unique, by At a limit point of the domain a function has at most one limit applied on the domain $A ∖ {c}$ , which is what makes $f^{'} (c)$ a name for one real number. Two further facts are established there because everything below uses them: a derivative survives shrinking the domain, provided the smaller domain still accumulates at the point; and every point of a nondegenerate interval is a limit point of it, so that on an interval the symbol $f^{'} (c)$ is meaningful at every point, endpoints included.

Carathéodory, and why every rule on this page is one line. Carathéodory's characterisation: $f$ is differentiable at $c$ if and only if there is $φ : A \to R$ , continuous at $c$ , with $f (x) - f (c) = φ (x) (x - c)$ for every $x \in A$ , and then $φ$ is unique and $φ (c) = f^{'} (c)$ replaces the quotient by an algebraic identity: $f$ is differentiable at $c$ exactly when some $φ : A \to R$ , continuous at $c$ , satisfies $f (x) - f (c) = φ (x) (x - c)$ throughout $A$ , and then $φ$ is unique with $φ (c) = f^{'} (c)$ . That reformulation is what carries the whole toolkit. A function differentiable at $c$ is continuous at $c$ becomes a product of two continuous factors; 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$ becomes four rearrangements of an increment, each followed by a reading of 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; and 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)$ becomes a single substitution, with none of the case analysis that a difference-quotient proof needs where the inner increment vanishes. The linear-approximation form of the derivative: $f$ is differentiable at $c$ with $f^{'} (c) = L$ if and only if the remainder $r (x) = f (x) - f (c) - L (x - c)$ satisfies $\lim_{x \to c} r (x) / (x - c) = 0$ ; at most one $L$ does so, so $x \mapsto f (c) + L (x - c)$ is the unique affine map approximating $f$ to first order at $c$ records the other standard reformulation, that $f^{'} (c)$ is the unique slope for which the affine approximation has remainder small compared with the increment.

The rules, and the index trap inside the power rule. For a natural $n \geq 1$ the function $x \mapsto x^{n}$ is differentiable everywhere with derivative $ι (n) x^{n - 1}$ ; for $n = 0$ it is the constant $1$ , with derivative $0$ ; for a natural $n \geq 1$ the function $x \mapsto x^{- n}$ is differentiable at every $x \neq 0$ with derivative $- ι (n) x^{- n - 1}$ ; consequently every polynomial function is differentiable at every real, with the derivative computed term by term proves that $x \mapsto x^{n}$ has derivative $ι (n) x^{n - 1}$ for every natural $n \geq 1$ , that $x \mapsto x^{0}$ is the constant $1$ with derivative $0$ , and that $x \mapsto x^{- n}$ has derivative $- ι (n) x^{- n - 1}$ away from $0$ ; the case $n = 0$ is stated separately and not folded into the general formula, because $ι (0) c^{- 1}$ is not defined at $c = 0$ . Polynomial functions follow by induction along the recursion defining finite sums. Derivative of an inverse: if $f$ is continuous and injective on a nondegenerate interval $I$ and differentiable at $c \in I$ with $f^{'} (c) \neq 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)$ closes the toolkit: at a point $f (c)$ where $f$ is differentiable, the inverse is differentiable exactly when $f^{'} (c)$ does not vanish, with the reciprocal derivative, and is not differentiable when it does; nothing is asserted at a point of $f [I]$ where $f$ itself has no derivative. Both halves rest on Continuous inverse theorem: a continuous injective $f$ on an interval $I$ is a bijection onto the order-convex set $f [I]$ , and the inverse $g : f [I] \to I$ is continuous and strictly monotone in the same sense as $f$ , which supplies the inverse and its continuity, and the second half is a one-line use of the chain rule against the identity.

Extrema, and the theorem that needs an interior point. Local (relative) maximum and minimum of $f : A \to R$ at a point, the strict forms, and what it means for the point to be interior to $A$ fixes local maxima and minima, their strict forms, and what it means for a point to be interior to the domain; it also proves the two facts the theorems below need, that an interior point of a set is a limit point of it, which is what Fermat's theorem consumes, and that a global extremum is a local one, which is what Rolle's theorem consumes. Fermat's interior extremum theorem: if $f$ has a local extremum at a point $c$ interior to its domain and is differentiable at $c$ , then $f^{'} (c) = 0$ then shows that a derivative at an interior local extremum vanishes, by keeping the difference quotient on the sign of its limit (If $\lim_{x \to c} f (x) = L \neq 0$ then $∣ f ∣ > ∣ L ∣ / 2$ on a punctured neighbourhood of $c$ ; in particular if $L > 0$ then $f > L / 2 > 0$ there) and reading it on both sides of the point. The interiority hypothesis is exactly what places points of the domain on both sides, and it is not decoration: the companion page exhibits a function on $[0, 1]$ with extrema at both endpoints and derivative $1$ at each.

Rolle, Cauchy, and the mean value 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)$ combines Fermat with Extreme value theorem: a continuous real function on a nonempty compact subset of $R$ attains a greatest and a least value: a continuous function on $[a, b]$ attains a greatest and a least value, and if neither is attained inside then the hypothesis $f (a) = f (b)$ makes the function constant, so any interior point serves. 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 is one application of Rolle to $λ g - μ f$ with $λ = f (b) - f (a)$ and $μ = g (b) - g (a)$ , and it is stated as a product identity, $(f (b) - f (a)) g^{'} (c) = (g (b) - g (a)) f^{'} (c)$ , with no hypothesis on $g^{'}$ ; the familiar quotient form is not equivalent, and the companion page shows a pair for which it is meaningless while the product form holds. The mean value theorem, as the case $g (x) = x$ of Cauchy's: for $f$ continuous on $[a, b]$ with $a < b$ and differentiable on $(a, b)$ there is $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$ is the case $g (x) = x$ .

What the mean value theorem buys. Three consequences, each with the interval hypothesis doing real work. A function continuous on an interval $I$ whose derivative vanishes at every interior point of $I$ is constant on $I$ ; consequently two such functions with the same derivative differ by a constant: a function continuous on an interval with vanishing derivative at every interior point is constant, so two functions with the same derivative differ by a constant. On an interval $I$ , for $f$ continuous on $I$ and differentiable at every interior point: $f^{'} \geq 0$ throughout gives $f$ nondecreasing, $f^{'} > 0$ gives $f$ increasing, $f^{'} \leq 0$ and $f^{'} < 0$ give the two decreasing forms; conversely a nondecreasing $f$ has $f^{'} \geq 0$ and a nonincreasing $f$ has $f^{'} \leq 0$ wherever it is differentiable, and no strict converse is claimed: the four sign conditions on $f^{'}$ give the four monotonicity conditions of Nondecreasing, increasing (strictly increasing), nonincreasing, decreasing, monotone and strictly monotone real functions on a subset of $R$ , with the dictionary to monotone sequences, and conversely a nondecreasing function has $f^{'} \geq 0$ wherever it is differentiable. That converse is non-strict, and no strict form holds. If $f$ is continuous on an interval $I$ and $∣ f^{'} ∣ \leq M$ at every interior point, then $∣ f (x) - f (y) ∣ \leq M ∣ x - y ∣$ for all $x, y \in I$ , so $f$ is Lipschitz with constant $M$ and uniformly continuous on $I$ : a bound $∣ f^{'} ∣ \leq M$ at every interior point gives $∣ f (x) - f (y) ∣ \leq M ∣ x - y ∣$ throughout, so the function is Lipschitz with constant $M$ and, through Dictionary: for $A \subseteq R$ with the metric $d (x, y) = ∣ x - y ∣$ , continuity and uniform continuity of $f : A \to R$ agree with the metric-space notions, the Lipschitz and Hölder conditions are the metric ones instantiated, and a subset of $R$ is compact in the open-cover sense of $R$ exactly when it is a compact metric subspace and Contraction implies Lipschitz implies uniformly continuous implies continuous; every Hölder map is uniformly continuous, and a Lipschitz map on a bounded space is Hölder for every exponent, uniformly continuous.

Two false statements, both with witnesses. FALSE: differentiability at every point of $(a, b)$ alone yields a $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$ deletes the continuity hypothesis from the mean value theorem and is refuted by $f (x) = x$ on $[0, 1)$ with $f (1) = 0$ , which is differentiable at every interior point with derivative $1$ while $f (1) - f (0) = 0$ ; the same witness kills Rolle's theorem under the same weakening. FALSE: if $f^{'} (c) = 0$ then $f$ is not increasing on any interval containing $c$ reads the monotonicity theorem backwards and is refuted by $x \mapsto x^{3}$ , which is increasing on $R$ with $f^{'} (0) = 0$ .

What this page does not fix. No one-sided derivative and no derivative of order above one is defined here, and no item on this page says anything about the continuity of $f^{'}$ or about the existence of an antiderivative. Darboux's theorem is not proved here either, so nothing below says that $f^{'}$ has the intermediate value property of The intermediate value property (Darboux property) of a function on an interval: the image of every subinterval is order-convex. The monotone-functions page names that theorem as the classical source of discontinuous functions with the intermediate value property and builds its own witness by hand instead; this page does not discharge it, and no item here may be cited for it. Nothing on either page depends on it. What is fixed here and what is not: the derivative is taken at a point of the domain that is also a limit point of it, one-sided derivatives and derivatives of order above one are not introduced at this point in the reading order, and $f^{'} (c)$ and $\frac{d f}{d x} (c)$ name the same real number records exactly what is settled and what is left open, including that $f^{'} (c)$ and $\frac{d f}{d x} (c)$ name the same real number and that the second is a name and not a quotient.

3 · Logical flowchart

4 · Definitions, theorems and proofs

DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (z-ai/glm-5.2)audited 2026-07-28Open item page →

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

Definition

Throughout, $R$ is the complete ordered field (Complete ordered field (least-upper-bound property)), neighbourhoods are those of The $ε$ -neighbourhood and the punctured $ε$ -neighbourhood of a point of $R$ and limit points those of Limit point, isolated point, adherent point, derived set, and dense subset of $R$ .

Let $A \subseteq R$ , let $f : A \to R$ and let $c \in A$ be a limit point of $A$ . The difference quotient of $f$ at $c$ is the function

$q_{f, c} : A ∖ {c} \to R, q_{f, c} (x) : = \frac{f (x) - f (c)}{x - c} .$

The division is legitimate at every point of the domain, since $x \neq c$ gives $x - c \neq 0$ .

The point $c$ is a limit point of $A ∖ {c}$ , not merely of $A$ . For every real $ε > 0$ the punctured neighbourhood $N_{ε}^{*} (c)$ omits $c$ , so

$N_{ε}^{*} (c) \cap A = N_{ε}^{*} (c) \cap (A ∖ {c}),$

and the left-hand side is nonempty because $c$ is a limit point of $A$ . So $q_{f, c}$ is a function on a set having $c$ as a limit point, and $\lim_{x \to c} q_{f, c} (x)$ is a notion that The $ε$ - $δ$ limit $\lim_{x \to c} f (x) = L$ of $f : A \to R$ at a limit point $c$ of $A$ defines.

$f$ is differentiable at $c$ when that limit exists, and then the derivative of $f$ at $c$ is

$f^{'} (c) : = \lim_{x \to c} q_{f, c} (x) = \lim_{x \to c} \frac{f (x) - f (c)}{x - c} .$

Two obligations are carried by that notation, and both are discharged here.

Uniqueness. Writing $f^{'} (c)$ treats the right-hand side as a name for a single real number. That is legitimate: $c$ is a limit point of the domain $A ∖ {c}$ of $q_{f, c}$ , so at most one real can satisfy the $ε$ - $δ$ condition, by At a limit point of the domain a function has at most one limit applied to $q_{f, c}$ . Two reals both meeting the condition are therefore equal, and the symbol denotes.
Meaningfulness. The hypothesis that $c$ is a limit point of $A$ is not decoration. At an isolated point of $A$ the punctured condition $0 < ∣ x - c ∣ < δ$ is met by no point of the domain at all, so the $ε$ - $δ$ formula is satisfied vacuously by every real at once; this is why The $ε$ - $δ$ limit $\lim_{x \to c} f (x) = L$ of $f : A \to R$ at a limit point $c$ of $A$ leaves the limit undefined there, and it is why this library defines $f^{'} (c)$ only at a limit point of $A$ . At an isolated point of its domain a function is neither differentiable nor non-differentiable here: the question is not posed.

The limit sees only $A ∖ {c}$ , so how the difference quotient is extended to $c$ is irrelevant. Let $Q : A \to R$ agree with $q_{f, c}$ at every point of $A ∖ {c}$ , and let $L \in R$ . Then $\lim_{x \to c} Q (x) = L$ if and only if $\lim_{x \to c} q_{f, c} (x) = L$ . Both conditions read: for every real $ε > 0$ there is a real $δ > 0$ such that every point $x$ of the relevant domain with $0 < ∣ x - c ∣ < δ$ satisfies $∣ \cdot - L ∣ < ε$ (The $ε$ - $δ$ limit $\lim_{x \to c} f (x) = L$ of $f : A \to R$ at a limit point $c$ of $A$ ). The clause $0 < ∣ x - c ∣$ removes $x = c$ from both quantifiers, so in both cases the points quantified over are exactly the $x \in A ∖ {c}$ with $0 < ∣ x - c ∣ < δ$ , at which $Q$ and $q_{f, c}$ take the same value. The two conditions are the same condition.

Differentiability on a set. For $S \subseteq A$ , $f$ is differentiable on $S$ when it is differentiable at every $c \in S$ ; implicit in that phrase is that every point of $S$ is a limit point of $A$ . $f$ is differentiable when it is differentiable on the whole of $A$ .

Restriction of the domain. Let $B \subseteq A$ , let $c \in B$ and suppose $c$ is a limit point of $B$ . If $f$ is differentiable at $c$ , then so is the restriction $f ∣_{B} : B \to R$ , and

$(f ∣_{B})^{'} (c) = f^{'} (c) .$

Indeed $B ∖ {c} \subseteq A ∖ {c}$ ; the displayed identity of punctured neighbourhoods above, applied to $B$ , shows that $c$ is a limit point of $B ∖ {c}$ ; the difference quotient $q_{f ∣_{B}, c}$ is the restriction of $q_{f, c}$ to $B ∖ {c}$ , since $f ∣_{B} (c) = f (c)$ ; and claim 2 of The limit at $c$ depends only on the restriction of $f$ to a punctured neighbourhood of $c$ , and passes to any subset of the domain having $c$ as a limit point carries the limit to that restriction.

Every point of a nondegenerate interval is a limit point of it. Let $J \subseteq R$ be order-convex (Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length) with at least two elements and let $p \in J$ . Choose $q \in J$ with $q \neq p$ , and let a real $ε > 0$ be given. If $p < q$ , put $y : = p + \frac{1}{2} \min {ε, q - p}$ ; then $p < y$ , and $y - p \leq \frac{1}{2} (q - p) < q - p$ , so $p < y < q$ and order-convexity gives $y \in J$ , while $0 < ∣ y - p ∣ < ε$ . If $q < p$ , the point $y : = p - \frac{1}{2} \min {ε, p - q}$ serves in the same way. So $N_{ε}^{*} (p) \cap J \neq \emptyset$ for every real $ε > 0$ , that is, $p$ is a limit point of $J$ (Limit point, isolated point, adherent point, derived set, and dense subset of $R$ ).

Consequently, for $f$ defined on a nondegenerate interval $I$ , the symbol $f^{'} (c)$ is meaningful at every $c \in I$ , endpoints included. At an endpoint the difference quotient is taken over the points of $I$ lying on the one side that is available, so what other texts call a one-sided derivative is, here, simply the derivative of $f$ on $I$ .

Remarks

Notation. $f^{'} (c)$ and $\frac{d f}{d x} (c)$ denote the same real number, and this library uses the first. Neither is an operation performed on a symbol $x$ : the variable in the second is a name for the argument and nothing more.
Differentiability is a property of the pair $(f, A)$ at $c$ , not of $f$ alone. The restriction clause above goes in one direction only, and the converse fails. Take $A : = R$ , $f (x) : = ∣ x ∣$ , $B : = [0, \infty)$ and $c : = 0$ . Then $f ∣_{B}$ is the identity on $B$ , whose difference quotient at $0$ is constantly $1$ , so $f ∣_{B}$ is differentiable at $0$ with derivative $1$ ; that $f$ itself is not differentiable at $0$ is $x \mapsto ∣ x ∣$ is continuous everywhere and not differentiable at $0$ : the difference quotient equals $1$ on the right and $- 1$ on the left, so the two one-sided limits differ ↗ on the companion page. So enlarging the domain can destroy differentiability, and the phrase " $f$ is differentiable at $c$ " always carries the domain with it.
The relation to continuity is not definitional. 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 is a condition on $f$ near $c$ that does not mention a quotient, and it is defined at every point of $A$ , isolated points included, whereas differentiability is defined only at limit points of $A$ . That differentiability implies continuity is a theorem on this page and not a reading of the definitions.
No second derivative and no one-sided derivative is introduced here. Both are standard, and both are absent from this page on purpose; What is fixed here and what is not: the derivative is taken at a point of the domain that is also a limit point of it, one-sided derivatives and derivatives of order above one are not introduced at this point in the reading order, and $f^{'} (c)$ and $\frac{d f}{d x} (c)$ name the same real number records exactly what is fixed and what is left open at this point in the reading order.

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-28Open item page →

Carathéodory's characterisation: $f$ is differentiable at $c$ if and only if there is $φ : A \to R$ , continuous at $c$ , with $f (x) - f (c) = φ (x) (x - c)$ for every $x \in A$ , and then $φ$ is unique and $φ (c) = f^{'} (c)$

Statement

Let $A \subseteq R$ , let $f : A \to R$ and let $c \in A$ be a limit point of $A$ (Limit point, isolated point, adherent point, derived set, and dense subset of $R$ ). The following are equivalent.

$f$ is differentiable at $c$ (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).
There is a function $φ : A \to R$ , continuous at $c$ (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), with $f (x) - f (c) = φ (x) (x - c) for every x \in A .$

When they hold, the function $φ$ of claim 2 is unique and satisfies $φ (c) = f^{'} (c)$ .

What the reformulation buys. Claim 2 contains no quotient and no limit: it is an algebraic identity plus a continuity hypothesis at one point. Every differentiation rule on this page is proved by exhibiting the factor $φ$ for the new function and reading its continuity off the algebra and composition theorems for continuous functions. In particular the chain rule becomes a one-line substitution, with none of the case analysis that the difference-quotient proof needs where the inner increment vanishes.

The hypothesis that $c$ is a limit point of $A$ is used in both directions. It is what makes $f^{'} (c)$ a defined symbol at all (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), and it is what makes continuity of $φ$ at $c$ equivalent to a statement about the limit of $φ$ there (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, clause 1). At an isolated point of $A$ claim 2 holds for every $f$ , with $φ$ arbitrary off $c$ , because every function is continuous at an isolated point; claim 1 is not even a statement there.

Facts & Assumptions

Given: A set $A \subseteq R$ , a function $f : A \to R$ and a point $c \in A$ that is a limit point of $A$ (Limit point, isolated point, adherent point, derived set, and dense subset of $R$ ).

[L1]

Differentiability at $c$ (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): the difference quotient $q (x) : = (f (x) - f (c)) / (x - c)$ is a function on $A ∖ {c}$ , the point $c$ is a limit point of $A ∖ {c}$ , and $f$ is differentiable at $c$ exactly when $\lim_{x \to c} q (x)$ exists, its value then being $f^{'} (c)$ ; moreover, for any $Q : A \to R$ agreeing with $q$ on $A ∖ {c}$ and any real $L$ , the conditions $\lim_{x \to c} Q (x) = L$ and $\lim_{x \to c} q (x) = L$ are the same condition, since the clause $0 < ∣ x - c ∣$ removes $x = c$ from both quantifiers.

[L2]

The limit condition (The $ε$ - $δ$ limit $\lim_{x \to c} f (x) = L$ of $f : A \to R$ at a limit point $c$ of $A$ ): $\lim_{x \to c} h (x) = L$ means that for every real $ε > 0$ there is a real $δ > 0$ such that every $x$ in the domain of $h$ with $0 < ∣ x - c ∣ < δ$ satisfies $∣ h (x) - L ∣ < ε$ .

[L3]

Continuity at a limit point (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, clause 1): for $c \in A$ a limit point of $A$ , a function $ψ : A \to R$ is continuous at $c$ if and only if $\lim_{x \to c} ψ (x)$ exists and equals $ψ (c)$ .

[L4]

At a limit point of its domain a function has at most one limit (At a limit point of the domain a function has at most one limit).

[L5]

Locality (claim 1 of The limit at $c$ depends only on the restriction of $f$ to a punctured neighbourhood of $c$ , and passes to any subset of the domain having $c$ as a limit point): if two functions on $A$ agree at every $x \in A$ with $0 < ∣ x - c ∣ < η$ for some real $η > 0$ , then for every real $L$ one has $\lim_{x \to c} = L$ for the first exactly when it holds for the second.

Proof

technique · direct

1.1

Claim 1 implies claim 2: the factor. Assume $f$ is differentiable at $c$ , and define $φ : A \to R$ by $φ (x) : = (f (x) - f (c)) / (x - c)$ for $x \in A$ with $x \neq c$ , and $φ (c) : = f^{'} (c)$ . This is a function on the whole of $A$ , since every $x \in A$ falls under exactly one of the two clauses and the division is by a nonzero number.

L1construct

1.2

Claim 2 implies claim 1: the hypothesis. Assume instead that some $φ : A \to R$ is continuous at $c$ and satisfies $f (x) - f (c) = φ (x) (x - c)$ for every $x \in A$ .

assume-hyp

1.3

Uniqueness. Let $φ$ and $ψ$ both be as in claim 2. For $x \in A$ with $x \neq c$ the identity gives $φ (x) (x - c) = f (x) - f (c) = ψ (x) (x - c)$ , and dividing by $x - c \neq 0$ gives $φ (x) = ψ (x)$ ; so the two agree on $A ∖ {c}$ , hence at every $x \in A$ with $0 < ∣ x - c ∣ < 1$ . By [L3] each has a limit at $c$ , equal to its own value there; by [L5] those two limits are limits of functions agreeing near $c$ , so by [L4] they are equal, that is $φ (c) = ψ (c)$ . Hence $φ = ψ$ .

L3L4L5

2.1

The identity holds for the factor built in step 1.1. For $x \in A$ with $x \neq c$ , multiplying the defining equation $φ (x) = (f (x) - f (c)) / (x - c)$ by $x - c$ gives $φ (x) (x - c) = f (x) - f (c)$ ; and at $x = c$ both sides are $0$ , since $f (c) - f (c) = 0$ and $φ (c) (c - c) = 0$ . So the identity of claim 2 holds for every $x \in A$ .

step 1.1

2.2

The factor built in step 1.1 is continuous at $c$ . That $φ$ agrees with the difference quotient $q$ at every point of $A ∖ {c}$ is its definition, so by [L1] the limit $\lim_{x \to c} φ (x)$ exists and equals $f^{'} (c)$ , which is $φ (c)$ . Since $c$ is a limit point of $A$ , [L3] turns that into continuity of $φ$ at $c$ .

step 1.1L1L3

2.3

Under the hypothesis of step 1.2, $φ$ extends the difference quotient. For $x \in A$ with $x \neq c$ , dividing the identity by $x - c \neq 0$ gives $q (x) = φ (x) (x - c) / (x - c) = φ (x)$ . So $φ$ agrees with $q$ at every point of $A ∖ {c}$ .

step 1.2

2.4

Under the hypothesis of step 1.2, $φ$ has a limit at $c$ . Continuity of $φ$ at the limit point $c$ gives, by [L3], that $\lim_{x \to c} φ (x)$ exists and equals $φ (c)$ .

step 1.2L3

3.1

Claim 2 implies claim 1. By step 2.3 the function $φ$ agrees with $q$ off $c$ , so the last clause of [L1] applies with $Q : = φ$ and $L : = φ (c)$ : from $\lim_{x \to c} φ (x) = φ (c)$ , given by step 2.4, it follows that $\lim_{x \to c} q (x) = φ (c)$ . By [L1] again, $f$ is differentiable at $c$ and $f^{'} (c) = φ (c)$ .

step 2.3step 2.4L1L2

4.1

Both implications and both supplementary claims are proved: claim 1 gives claim 2 by steps 1.1, 2.1 and 2.2, with $φ (c) = f^{'} (c)$ by construction; claim 2 gives claim 1 by step 3.1, with $φ (c) = f^{'} (c)$ established there; and the factor is unique by step 1.3.

step 1.1step 1.3step 2.1step 2.2step 3.1∎

Remarks

The identity at $x = c$ is empty, and that is the point. Both sides vanish there whatever $φ (c)$ is, so the identity alone determines $φ$ only off $c$ ; it is the continuity hypothesis that pins the remaining value, and it pins it to $f^{'} (c)$ . Drop continuity and claim 2 becomes true for every $f$ whatsoever, with $φ (c)$ arbitrary.
Why this is not circular. The proof of claim 2 from claim 1 builds $φ$ out of the very quotient whose limit is $f^{'} (c)$ , so nothing new is asserted in that direction. The content is the other direction: a factorisation with a factor merely continuous at one point already forces the quotient to converge. That is the direction every rule on this page uses.
The factor is a genuinely useful object, not a device. For $f (x) = x^{n}$ it can be written down in closed form, as the polynomial $φ (x) = \sum_{k < n} c^{k} x^{n - 1 - k}$ supplied by Factorisation of $b^{n} - a^{n}$ , and the resulting Lipschitz estimate; the companion page writes that factor out and differentiates a composite with it.

CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-28Open item page →

A function differentiable at $c$ is continuous at $c$

Statement

Let $A \subseteq R$ , let $f : A \to R$ and let $c \in A$ be a limit point of $A$ (Limit point, isolated point, adherent point, derived set, and dense subset of $R$ ). If $f$ is differentiable at $c$ (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 $f$ is continuous at $c$ (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).

Consequently, if $f$ is differentiable on a set $S \subseteq A$ then $f$ is continuous at every point of $S$ .

No converse is asserted, and none holds. Continuity at $c$ does not give differentiability at $c$ , and the standard witness is worked out on the companion page.

Facts & Assumptions

Given: A set $A \subseteq R$ , a function $f : A \to R$ and a point $c \in A$ that is a limit point of $A$ at which $f$ is differentiable (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, Limit point, isolated point, adherent point, derived set, and dense subset of $R$ ).

[L1]

Carathéodory's characterisation (Carathéodory's characterisation: $f$ is differentiable at $c$ if and only if there is $φ : A \to R$ , continuous at $c$ , with $f (x) - f (c) = φ (x) (x - c)$ for every $x \in A$ , and then $φ$ is unique and $φ (c) = f^{'} (c)$ ): since $f$ is differentiable at the limit point $c$ of $A$ , there is $φ : A \to R$ , continuous at $c$ , with $f (x) - f (c) = φ (x) (x - c)$ for every $x \in A$ , and $φ (c) = f^{'} (c)$ .

[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): sums, scalar multiples and products of functions continuous at a point of the common domain are continuous there (claim 1); and every constant function on $A$ and the identity $x \mapsto x$ on $A$ are continuous at every point of $A$ (claim 5).

[L3]

Continuity of $f$ at $c$ is the $ε$ - $δ$ condition of 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, and continuity on a set is continuity at each of its points.

Proof

technique · direct

1.1

Fix a function $φ : A \to R$ , continuous at $c$ , with $f (x) - f (c) = φ (x) (x - c)$ for every $x \in A$ .

L1choose

1.2

The identity $x \mapsto x$ on $A$ and every constant function on $A$ are continuous at $c$ ; hence so is $x \mapsto x - c$ , which is the sum of the identity and the constant function with value $- c$ .

2.1

The pointwise product $x \mapsto φ (x) (x - c)$ is continuous at $c$ , being the product of two functions on $A$ continuous at $c$ .

step 1.1step 1.2L2

3.1

For every $x \in A$ one has $f (x) = f (c) + φ (x) (x - c)$ , so $f$ is the sum of the constant function with value $f (c)$ and the product of step 2.1.

step 1.1L1

4.1

A sum of two functions continuous at $c$ is continuous at $c$ , so $f$ is continuous at $c$ .

step 2.1step 3.1L2L3

5.1

The point $c$ was an arbitrary point of $A$ , a limit point of $A$ , at which $f$ is differentiable; applying step 4.1 at every point of a set $S \subseteq A$ on which $f$ is differentiable gives continuity of $f$ at every point of $S$ .

step 3.1L3∎

Remarks

Where the work actually is. None of it is here. Carathéodory's characterisation already replaces the quotient by a product, and a product is visibly small when one factor is bounded near $c$ and the other tends to $0$ ; the algebra of continuous functions packages exactly that. A direct proof from the quotient would multiply and divide by $x - c$ and would have to say why that is legal, which is the same observation in a less convenient place.
The converse fails. $x \mapsto ∣ x ∣$ is continuous at $0$ and not differentiable there, which is $x \mapsto ∣ x ∣$ is continuous everywhere and not differentiable at $0$ : the difference quotient equals $1$ on the right and $- 1$ on the left, so the two one-sided limits differ ↗ on the companion page. So continuity is strictly weaker, and the gap is not exotic: it opens at a single corner.
What is not claimed. Nothing here says that a function differentiable on a set has a continuous derivative, and nothing here says that $f^{'}$ is defined anywhere except where it was assumed to be. Both are separate questions, and neither is settled on this page.

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-28Open item page →

The linear-approximation form of the derivative: $f$ is differentiable at $c$ with $f^{'} (c) = L$ if and only if the remainder $r (x) = f (x) - f (c) - L (x - c)$ satisfies $\lim_{x \to c} r (x) / (x - c) = 0$ ; at most one $L$ does so, so $x \mapsto f (c) + L (x - c)$ is the unique affine map approximating $f$ to first order at $c$

Statement

Let $A \subseteq R$ , let $f : A \to R$ , let $c \in A$ be a limit point of $A$ (Limit point, isolated point, adherent point, derived set, and dense subset of $R$ ) and let $L \in R$ . Write

$α_{L} : A \to R, α_{L} (x) : = f (c) + L (x - c),$

for the affine map through $(c, f (c))$ of slope $L$ , and let $r_{L} : = f - α_{L}$ , that is $r_{L} (x) = f (x) - f (c) - L (x - c)$ .

$f$ is differentiable at $c$ with $f^{'} (c) = L$ (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) if and only if $\lim_{x \to c} \frac{r_{L} (x)}{x - c} = 0,$ the quotient being taken as a function on $A ∖ {c}$ (The $ε$ - $δ$ limit $\lim_{x \to c} f (x) = L$ of $f : A \to R$ at a limit point $c$ of $A$ ).
At most one real $L$ satisfies the condition of claim 1. Some real satisfies it exactly when $f$ is differentiable at $c$ , and then that real is $f^{'} (c)$ .

So among all affine maps through $(c, f (c))$ there is at most one whose error $r_{L}$ is small compared with $x - c$ near $c$ ; it exists exactly when $f$ is differentiable at $c$ , and its slope is the derivative. This is the sense in which the derivative is a first-order approximation and not merely a quotient.

What the statement does not say. It says nothing about how small $r_{L}$ is in absolute terms, and nothing about any $x$ away from $c$ . The assertion is only that the ratio $r_{L} (x) / (x - c)$ tends to $0$ ; a second-order estimate on $r_{L}$ needs hypotheses this page does not have.

Facts & Assumptions

Given: A set $A \subseteq R$ , a function $f : A \to R$ , a point $c \in A$ that is a limit point of $A$ , a real $L$ , and the functions $α_{L}$ and $r_{L} = f - α_{L}$ of the statement (Limit point, isolated point, adherent point, derived set, and dense subset of $R$ , 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).

[L1]

[L2]

The limit condition (The $ε$ - $δ$ limit $\lim_{x \to c} f (x) = L$ of $f : A \to R$ at a limit point $c$ of $A$ ): $\lim_{x \to c} h (x) = P$ means that for every real $ε > 0$ there is a real $δ > 0$ such that every $x$ in the domain of $h$ with $0 < ∣ x - c ∣ < δ$ satisfies $∣ h (x) - P ∣ < ε$ .

[L3]

At a limit point of its domain a function has at most one limit (At a limit point of the domain a function has at most one limit); in particular the value $f^{'} (c)$ is a single real.

[L4]

Absolute value: $∣ u - 0 ∣ = ∣ u ∣$ , since $u - 0 = u$ (Basic properties of the absolute value).

Proof

technique · direct

1.1

For every $x \in A$ with $x \neq c$ the number $x - c$ is nonzero, so the quotient $r_{L} (x) / (x - c)$ is defined, and $r_{L} (x) / (x - c) = (f (x) - f (c)) / (x - c) - L (x - c) / (x - c) = q (x) - L$ . So $x \mapsto r_{L} (x) / (x - c)$ and $x \mapsto q (x) - L$ are the same function on $A ∖ {c}$ .

L1algebra

2.1

Hence for every $x \in A$ with $x \neq c$ one has $∣ r_{L} (x) / (x - c) - 0 ∣ = ∣ q (x) - L ∣$ .

step 1.1L4

3.1

Fix a real $ε > 0$ and a real $δ > 0$ . By step 2.1 the assertion "every $x \in A ∖ {c}$ with $0 < ∣ x - c ∣ < δ$ satisfies $∣ r_{L} (x) / (x - c) - 0 ∣ < ε$ " and the assertion "every $x \in A ∖ {c}$ with $0 < ∣ x - c ∣ < δ$ satisfies $∣ q (x) - L ∣ < ε$ " are the same assertion. Quantifying over $ε$ and $δ$ , the two limit conditions of [L2] on the common domain $A ∖ {c}$ , of which $c$ is a limit point by [L1], coincide.

step 2.1L1L2

3.2

Therefore $\lim_{x \to c} r_{L} (x) / (x - c) = 0$ holds if and only if $\lim_{x \to c} q (x) = L$ holds, which by [L1] is exactly differentiability of $f$ at $c$ with $f^{'} (c) = L$ : claim 1.

step 2.1L1L2

4.1

Suppose reals $L$ and $L^{'}$ both satisfy the condition of claim 1. By step 3.2 the function $f$ is differentiable at $c$ with $f^{'} (c) = L$ and with $f^{'} (c) = L^{'}$ ; the derivative is a single real by [L1] and [L3], so $L = L^{'}$ . Conversely, if $f$ is differentiable at $c$ then $L : = f^{'} (c)$ satisfies the condition, again by step 3.2.

step 3.1step 3.2L1L3

5.1

Claims 1 and 2 are proved, the first by step 3.2 and the second by step 4.1; so the affine map $α_{L}$ with the stated approximation property is unique when it exists, and its slope is $f^{'} (c)$ .

step 3.2step 4.1∎

Remarks

Why this is worth stating separately. The quotient form is what one computes with; the remainder form is what generalises, since it never divides by the increment and so survives verbatim in settings where the increment is not a number one may divide by. Nothing on this page needs that generality, but the equivalence is what licenses the phrase "best linear approximation" used informally elsewhere, and the phrase is otherwise unearned.
The two forms are the same $ε$ - $δ$ condition, not two conditions that happen to agree. Step 1.1 is an identity of functions on $A ∖ {c}$ , and everything after it is bookkeeping. In particular the proof spends no limit theorem at all: no algebra of limits, no sequences and no choice principle.
Uniqueness is the whole of claim 2, and it is inherited. It comes from At a limit point of the domain a function has at most one limit, the same lemma that lets $f^{'} (c)$ be written at all (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). Without a limit point of the domain there is no uniqueness anywhere in sight, and the phrase "the best approximation" would name nothing.

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

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$

Statement

Let $A \subseteq R$ , let $c \in A$ be a limit point of $A$ (Limit point, isolated point, adherent point, derived set, and dense subset of $R$ ), let $f, g : A \to R$ be differentiable at $c$ (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) and let $α \in R$ . Then:

$f + g$ is differentiable at $c$ and $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ ;
$α f$ is differentiable at $c$ and $(α f)^{'} (c) = α f^{'} (c)$ ;
$f g$ is differentiable at $c$ and $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ ;
if $g (c) \neq 0$ then, writing $A_{0} : = {x \in A : g (x) \neq 0}$ , the point $c$ lies in $A_{0}$ and is a limit point of $A_{0}$ , the quotient $(f / g) ∣_{A_{0}} : A_{0} \to R$ , $x \mapsto f (x) / g (x)$ , is differentiable at $c$ as a function on $A_{0}$ , and $((f / g) ∣_{A_{0}})^{'} (c) = \frac{f^{'} (c) g (c) - f (c) g^{'} (c)}{g (c)^{2}} .$

Each claim asserts two things: that the derivative on the left exists, and that it has the stated value. Both are proved.

Why claim 4 is stated on $A_{0}$ . The function $f / g$ is not defined where $g$ vanishes, and $g$ may vanish at points of $A$ far from $c$ ; restricting to $A_{0}$ is forced. That the restriction still has $c$ as a limit point, so that a derivative there means anything at all, is not free either, and it is the last claim of If $\lim_{x \to c} f (x) = L \neq 0$ then $∣ f ∣ > ∣ L ∣ / 2$ on a punctured neighbourhood of $c$ ; in particular if $L > 0$ then $f > L / 2 > 0$ there applied to $g$ . The hypothesis is $g (c) \neq 0$ , not " $g$ vanishes nowhere".

Everything is proved through Carathéodory's characterisation: $f$ is differentiable at $c$ if and only if there is $φ : A \to R$ , continuous at $c$ , with $f (x) - f (c) = φ (x) (x - c)$ for every $x \in A$ , and then $φ$ is unique and $φ (c) = f^{'} (c)$ . No difference quotient is estimated and no limit theorem beyond continuity is used, so no choice principle is spent. The four identities are four algebraic rearrangements of an increment, each followed by a reading of 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.

Facts & Assumptions

Given: A set $A \subseteq R$ , a point $c \in A$ that is a limit point of $A$ , functions $f, g : A \to R$ differentiable at $c$ , and a real $α$ ; for claim 4 also the hypothesis $g (c) \neq 0$ together with $A_{0} : = {x \in A : g (x) \neq 0}$ (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, Limit point, isolated point, adherent point, derived set, and dense subset of $R$ ).

[L1]

Carathéodory's characterisation (Carathéodory's characterisation: $f$ is differentiable at $c$ if and only if there is $φ : A \to R$ , continuous at $c$ , with $f (x) - f (c) = φ (x) (x - c)$ for every $x \in A$ , and then $φ$ is unique and $φ (c) = f^{'} (c)$ ), used in both directions: for a set $B \subseteq R$ , a point $p \in B$ that is a limit point of $B$ and a function $h : B \to R$ , the function $h$ is differentiable at $p$ if and only if there is $η : B \to R$ , continuous at $p$ , with $h (x) - h (p) = η (x) (x - p)$ for every $x \in B$ , and then $η (p) = h^{'} (p)$ .

[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): sums, scalar multiples and products of functions continuous at a point are continuous there (claim 1); every constant function and the identity are continuous everywhere on the domain (claim 5); and if $u, v$ are continuous at a point $p$ of their common domain $D$ with $v (p) \neq 0$ , then $p$ lies in $D_{0} : = {x \in D : v (x) \neq 0}$ and $(u / v) ∣_{D_{0}}$ is continuous at $p$ as a function on $D_{0}$ (claim 4).

[L3]

Continuity passes to a subset of the domain: if $B \subseteq A$ , if $p \in B$ and if $ψ : A \to R$ is continuous at $p$ , then $ψ ∣_{B}$ is continuous at $p$ , the condition on the restriction quantifying over fewer points (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).

[L4]

A function differentiable at $c$ is continuous at $c$ (A function differentiable at $c$ is continuous at $c$ ); in particular $g$ is.

[L5]

At a limit point $c$ of $A$ , continuity of $g$ at $c$ says exactly that $\lim_{x \to c} g (x)$ exists and equals $g (c)$ (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, clause 1, The $ε$ - $δ$ limit $\lim_{x \to c} f (x) = L$ of $f : A \to R$ at a limit point $c$ of $A$ ).

[L6]

Sign preservation (If $\lim_{x \to c} f (x) = L \neq 0$ then $∣ f ∣ > ∣ L ∣ / 2$ on a punctured neighbourhood of $c$ ; in particular if $L > 0$ then $f > L / 2 > 0$ there): if $c$ is a limit point of $A$ and $\lim_{x \to c} g (x)$ exists and is nonzero, then $c$ is a limit point of $A_{0} = {x \in A : g (x) \neq 0}$ .

[L7]

A product of two nonzero reals is nonzero (A field has no zero divisors: $a b = 0 \Rightarrow a = 0$ or $b = 0$ ), and $g (c)^{2} = g (c) g (c)$ (Integer powers $a^{m}$ ).

Proof

technique · direct

1.1

By [L1], applied to $f$ and to $g$ on $A$ at $c$ , fix $φ, ψ : A \to R$ , both continuous at $c$ , with $f (x) - f (c) = φ (x) (x - c)$ and $g (x) - g (c) = ψ (x) (x - c)$ for every $x \in A$ , and with $φ (c) = f^{'} (c)$ and $ψ (c) = g^{'} (c)$ .

L1choose

1.2

Assume $g (c) \neq 0$ . Then $c \in A_{0}$ by the definition of $A_{0}$ ; $g$ is continuous at $c$ by [L4], so $\lim_{x \to c} g (x) = g (c) \neq 0$ by [L5]; and therefore $c$ is a limit point of $A_{0}$ by [L6].

L4L5L6

2.1

Sum. For every $x \in A$ , $(f + g) (x) - (f + g) (c) = (f (x) - f (c)) + (g (x) - g (c)) = (φ (x) + ψ (x)) (x - c)$ . The function $φ + ψ$ is continuous at $c$ by [L2], and $(φ + ψ) (c) = f^{'} (c) + g^{'} (c)$ . So [L1] gives claim 1.

step 1.1L1L2

2.2

Scalar multiple. For every $x \in A$ , $(α f) (x) - (α f) (c) = α (f (x) - f (c)) = (α φ (x)) (x - c)$ . The function $α φ$ is continuous at $c$ by [L2], with value $α f^{'} (c)$ there. So [L1] gives claim 2.

step 1.1L1L2

2.3

Product. For every $x \in A$ , $f (x) g (x) - f (c) g (c) = (f (x) - f (c)) g (x) + f (c) (g (x) - g (c)) = (φ (x) g (x) + f (c) ψ (x)) (x - c)$ . Put $χ : = φ g + f (c) ψ$ ; it is continuous at $c$ by [L2], since $φ$ , $ψ$ and (by [L4]) $g$ are, and constants are; and $χ (c) = φ (c) g (c) + f (c) ψ (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ . So [L1] gives claim 3.

step 1.1L1L2L4

2.4

Quotient, the rearrangement. Assume $g (c) \neq 0$ and let $x \in A_{0}$ , so $g (x) \neq 0$ and $g (c) \neq 0$ . Then $f (x) / g (x) - f (c) / g (c) = (f (x) g (c) - f (c) g (x)) / (g (x) g (c))$ , and $f (x) g (c) - f (c) g (x) = (f (x) - f (c)) g (c) - f (c) (g (x) - g (c)) = (φ (x) g (c) - f (c) ψ (x)) (x - c)$ . So, defining $θ : A_{0} \to R$ by $θ (x) : = (φ (x) g (c) - f (c) ψ (x)) / (g (x) g (c))$ , one has $(f / g) ∣_{A_{0}} (x) - (f / g) ∣_{A_{0}} (c) = θ (x) (x - c)$ for every $x \in A_{0}$ .

step 1.1L1L7

2.5

Quotient, continuity of the factor. Assume $g (c) \neq 0$ . The restrictions of $φ$ , $ψ$ and $g$ to $A_{0}$ are continuous at $c \in A_{0}$ by [L3] and [L4], so by [L2] the numerator $u (x) : = φ (x) g (c) - f (c) ψ (x)$ and the denominator $v (x) : = g (x) g (c)$ are continuous at $c$ as functions on $A_{0}$ . By [L7] the denominator vanishes at no point of $A_{0}$ , so ${x \in A_{0} : v (x) \neq 0} = A_{0}$ , and $v (c) = g (c)^{2} \neq 0$ ; hence claim 4 of [L2] gives that $θ = (u / v) ∣_{A_{0}}$ is continuous at $c$ , with $θ (c) = (φ (c) g (c) - f (c) ψ (c)) / g (c)^{2} = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ .

step 1.1step 1.2L2L3L4L7

3.1

Quotient, conclusion. Assume $g (c) \neq 0$ . By step 1.2 the point $c$ lies in $A_{0}$ and is a limit point of $A_{0}$ ; by steps 2.4 and 2.5 the function $θ : A_{0} \to R$ is continuous at $c$ and factors the increment of $(f / g) ∣_{A_{0}}$ . So [L1], applied on the domain $A_{0}$ at the point $c$ , gives that $(f / g) ∣_{A_{0}}$ is differentiable at $c$ with derivative $θ (c)$ : claim 4.

step 1.2step 2.4step 2.5L1

4.1

Claims 1 to 4 are proved, by steps 2.1, 2.2, 2.3 and 3.1 respectively, each by exhibiting the Carathéodory factor of the new function and reading its continuity at $c$ off the algebra of continuous functions.

step 2.1step 2.2step 2.3step 3.1∎

Remarks

The product rearrangement in one line. The identity $f g - f (c) g (c) = (f - f (c)) g + f (c) (g - g (c))$ splits the increment of a product into two increments, one multiplied by $g$ and one by a constant. It is the same identity that carries the product case of Sums, scalar multiples, products and quotients of function limits, the quotient under the hypothesis that the denominator limit is nonzero, read at the level of increments rather than of $ε$ ; here the factor $g$ has to be continuous at $c$ rather than merely bounded near it, and A function differentiable at $c$ is continuous at $c$ is what supplies that.
The reciprocal is the case $f \equiv 1$ . Claim 4 then reads $((1 / g) ∣_{A_{0}})^{'} (c) = - g^{'} (c) / g (c)^{2}$ , since $f^{'} (c) = 0$ for a constant $f$ ; nothing separate has to be proved, and the derivative of a negative integer power on this page is obtained exactly this way.
Two hypotheses that look removable and are not. In claim 4 the hypothesis $g (c) \neq 0$ cannot be weakened to " $g$ is nonzero somewhere near $c$ ", because $c$ itself must lie in the smaller domain for a derivative there to be a statement about $c$ ; and the conclusion is about $(f / g) ∣_{A_{0}}$ , not about any extension of it to $A$ , since no such extension is canonical.

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-28Open item page →

For a natural $n \geq 1$ the function $x \mapsto x^{n}$ is differentiable everywhere with derivative $ι (n) x^{n - 1}$ ; for $n = 0$ it is the constant $1$ , with derivative $0$ ; for a natural $n \geq 1$ the function $x \mapsto x^{- n}$ is differentiable at every $x \neq 0$ with derivative $- ι (n) x^{- n - 1}$ ; consequently every polynomial function is differentiable at every real, with the derivative computed term by term

Statement

Powers are those of Integer powers $a^{m}$ , and $ι : N \to R$ is the canonical natural of The canonical natural $ι (n) = n \cdot 1_{F}$ of a field, so that $ι (0) = 0$ and $ι (m + 1) = ι (m) + 1$ . Let $n \in N$ .

The function $p_{0} : R \to R$ , $p_{0} (x) = x^{0}$ , is the constant function $1$ , and it is differentiable at every $c \in R$ with $p_{0}^{'} (c) = 0$ (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).
For $n \geq 1$ the function $p_{n} : R \to R$ , $p_{n} (x) = x^{n}$ , is differentiable at every $c \in R$ , and $p_{n}^{'} (c) = ι (n) c^{n - 1} .$
For $n \geq 1$ put $A_{0} : = {x \in R : x \neq 0}$ . The function $m_{n} : A_{0} \to R$ , $m_{n} (x) = x^{- n}$ , is differentiable at every $c \in A_{0}$ as a function on $A_{0}$ , and $m_{n}^{'} (c) = - ι (n) c^{- n - 1} .$
Let $a : N \to R$ with $a_{j} = 0$ for $j \geq n$ , and let $P : R \to R$ be the polynomial function $P (x) = \sum_{j < n} a_{j} x^{j}$ (Finite sums and finite products, by recursion). Then $P$ is differentiable at every $c \in R$ , and, defining $e : N \to R$ by $e_{0} : = 0$ and $e_{j} : = ι (j) a_{j} c^{j - 1}$ for $j \geq 1$ , $P^{'} (c) = \sum_{j < n} e_{j} .$

Claim 2 is stated for $n \geq 1$ and not for $n \geq 0$ , and that is not timidity. At $n = 0$ its right-hand side reads $ι (0) c^{- 1}$ , and $c^{- 1}$ is not defined at $c = 0$ (Integer powers $a^{m}$ ), so the formula is not a statement about the whole line. Claim 1 is what covers $n = 0$ , and it says the derivative is $0$ there, which is what the informal reading " $0 \cdot c^{- 1}$ " is reaching for. The same shift is why the term $e_{0}$ of claim 4 is defined to be $0$ outright rather than by the formula.

Facts & Assumptions

Given: A natural $n$ , a real $c$ , and the functions $p_{n}$ , $m_{n}$ and $P$ of the statement.

[L1]

Powers (Integer powers $a^{m}$ ): $a^{0} = 1$ and $a^{m + 1} = a^{m} a$ for every $a \in R$ and $m \in N$ ; $a^{- m} : = (a^{m})^{- 1}$ for $a \neq 0$ and $m \geq 1$ ; and $0^{m} = 0$ for $m \geq 1$ .

[L2]

Canonical naturals (The canonical natural $ι (n) = n \cdot 1_{F}$ of a field): $ι (0) = 0$ , $ι (m + 1) = ι (m) + 1$ , and hence $ι (1) = 1$ .

[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$ ): at a limit point $c$ of the common domain, sums, scalar multiples and products of functions differentiable at $c$ are differentiable at $c$ with the four stated formulas, and if the denominator is nonzero at $c$ then the quotient, restricted to the set where the denominator does not vanish, is differentiable at $c$ with the quotient formula; that restricted set has $c$ as a limit point.

[L4]

Derivative and difference quotient (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): $f$ is differentiable at a limit point $c$ of its domain $D$ exactly when the difference quotient $x \mapsto (f (x) - f (c)) / (x - c)$ , a function on $D ∖ {c}$ , has a limit at $c$ , and $f^{'} (c)$ is that limit. A constant function $h \equiv K$ on a set having $c$ as a limit point has $\lim_{x \to c} h (x) = K$ : given a real $ε > 0$ , any real $δ > 0$ serves, since $∣ K - K ∣ = 0 < ε$ (The $ε$ - $δ$ limit $\lim_{x \to c} f (x) = L$ of $f : A \to R$ at a limit point $c$ of $A$ ).

[L5]

Induction principle on $N$ (The principle of mathematical induction).

[L6]

Finite sums (Finite sums and finite products, by recursion): $\sum_{j < 0} b_{j} = 0$ and $\sum_{j < m + 1} b_{j} = (\sum_{j < m} b_{j}) + b_{m}$ .

[L7]

Integer exponent laws for a nonzero base (Laws of integer exponents): $a^{k} \neq 0$ for every $k \in N$ when $a \neq 0$ ; and for integers $j, k$ one has $a^{j} a^{k} = a^{j + k}$ , $(a^{j})^{k} = a^{j k}$ and $a^{- k} = (a^{k})^{- 1}$ .

[L8]

Every real is a limit point of $R$ , punctured neighbourhoods in $R$ being never empty (Limit point, isolated point, adherent point, derived set, and dense subset of $R$ , The $ε$ -neighbourhood and the punctured $ε$ -neighbourhood of a point of $R$ ).

Proof

technique · induction

1.1

Base case, claim 2 at $n = 1$ . By [L1], $x^{1} = x^{0} x = 1 \cdot x = x$ , so $p_{1}$ is the identity. Fix $c \in R$ ; for every $x \neq c$ the difference quotient is $(x - c) / (x - c) = 1$ , so it is the constant function $1$ on $R ∖ {c}$ , and by [L4] and [L8] its limit at $c$ is $1$ . Since $ι (1) c^{0} = 1 \cdot 1 = 1$ by [L1] and [L2], claim 2 holds at $n = 1$ .

baseL1L2L4L8

1.2

Inductive hypothesis. Fix a natural $n \geq 1$ and assume that $p_{n}$ is differentiable at every $c \in R$ with $p_{n}^{'} (c) = ι (n) c^{n - 1}$ .

1.3

Claim 1. By [L1] the function $p_{0}$ is the constant function $1$ . Fix $c \in R$ ; for every $x \neq c$ its difference quotient is $(1 - 1) / (x - c) = 0$ , the constant function $0$ on $R ∖ {c}$ , whose limit at $c$ is $0$ by [L4] and [L8]. So $p_{0}$ is differentiable at every $c$ with $p_{0}^{'} (c) = 0$ .

L1L4L8

2.1

Successor step. Let $c \in R$ . By [L1], $p_{n + 1} (x) = x^{n + 1} = x^{n} x = p_{n} (x) p_{1} (x)$ for every $x$ . Both factors are differentiable at $c$ , by step 1.2 and step 1.1, so the product rule of [L3] gives that $p_{n + 1}$ is differentiable at $c$ with $p_{n + 1}^{'} (c) = p_{n}^{'} (c) p_{1} (c) + p_{n} (c) p_{1}^{'} (c) = ι (n) c^{n - 1} c + c^{n} \cdot 1$ . Now $c^{n - 1} c = c^{(n - 1) + 1} = c^{n}$ by [L1], so the right-hand side is $ι (n) c^{n} + c^{n} = (ι (n) + 1) c^{n} = ι (n + 1) c^{n}$ by [L2].

step 1.1step 1.2L1L2L3

3.1

Claim 2. Steps 1.1 and 2.1 are the base case and the successor step of an induction over the naturals $n \geq 1$ , so by [L5] the function $p_{n}$ is differentiable at every $c \in R$ with $p_{n}^{'} (c) = ι (n) c^{n - 1}$ , for every natural $n \geq 1$ .

step 1.1step 2.1L5

4.1

Claim 3. Let $n \geq 1$ . The set ${x \in R : p_{n} (x) \neq 0}$ is exactly $A_{0}$ : a nonzero $x$ has $x^{n} \neq 0$ by [L7], and $0^{n} = 0$ by [L1]. Fix $c \in A_{0}$ . The constant function $1$ on $R$ is differentiable at $c$ with derivative $0$ by step 1.3, and $p_{n}$ is differentiable at $c$ with derivative $ι (n) c^{n - 1}$ by step 3.1, with $p_{n} (c) = c^{n} \neq 0$ . So the quotient rule of [L3] applies: the function $x \mapsto 1 / x^{n}$ on $A_{0}$ , which by [L1] and [L7] is $m_{n}$ , is differentiable at $c$ with derivative $(0 \cdot c^{n} - 1 \cdot ι (n) c^{n - 1}) / (c^{n})^{2} = - ι (n) c^{n - 1} (c^{2 n})^{- 1} = - ι (n) c^{n - 1 - 2 n} = - ι (n) c^{- n - 1}$ , where $(c^{n})^{2} = c^{2 n}$ and $c^{n - 1} c^{- 2 n} = c^{- n - 1}$ are [L7].

step 1.3step 3.1L1L3L7

4.2

Claim 4, by a second induction on $n$ . Fix $c \in R$ and the sequence $a$ . At $n = 0$ the sum $P (x) = \sum_{j < 0} a_{j} x^{j}$ is $0$ for every $x$ by [L6], so $P$ is the constant function $0$ and, as in step 1.3, $P^{'} (c) = 0 = \sum_{j < 0} e_{j}$ . Suppose the claim holds at $n$ , and let $P_{n + 1} (x) : = \sum_{j < n + 1} a_{j} x^{j}$ . By [L6], $P_{n + 1} (x) = P_{n} (x) + a_{n} x^{n}$ for every $x$ , where $P_{n} (x) = \sum_{j < n} a_{j} x^{j}$ . The function $x \mapsto a_{n} x^{n}$ is differentiable at $c$ with derivative $e_{n}$ : for $n = 0$ it is the constant $a_{n}$ , of derivative $0 = e_{0}$ , by step 1.3 and the scalar rule of [L3]; for $n \geq 1$ it is the scalar multiple $a_{n} p_{n}$ , of derivative $a_{n} ι (n) c^{n - 1} = e_{n}$ , by step 3.1 and the scalar rule of [L3]. The inductive hypothesis gives $P_{n}^{'} (c) = \sum_{j < n} e_{j}$ , so the sum rule of [L3] gives that $P_{n + 1}$ is differentiable at $c$ with $P_{n + 1}^{'} (c) = \sum_{j < n} e_{j} + e_{n} = \sum_{j < n + 1} e_{j}$ by [L6]. By [L5] claim 4 holds for every $n \in N$ .

step 1.3step 3.1L3L5L6

5.1

All four claims are established: claim 1 by step 1.3, claim 2 by step 3.1, claim 3 by step 4.1 and claim 4 by step 4.2.

step 1.3step 3.1step 4.1step 4.2discharge-induction∎

Remarks

Why the induction starts at $n = 1$ and not at $n = 0$ . The successor step multiplies by the identity, and the identity is $p_{1}$ ; starting at $n = 0$ would require the formula of claim 2 to hold at $n = 0$ , which it does not, since $c^{- 1}$ is undefined at $c = 0$ . The two statements are therefore kept apart, and claim 1 is proved on its own from the definition. This is the same index care that The canonical natural $ι (n) = n \cdot 1_{F}$ of a field records for families of reciprocals: $N$ contains $0$ , and a formula written for " $n$ " is a claim about $n = 0$ unless it says otherwise.
The negative exponents cost nothing extra. Claim 3 is the quotient rule of 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$ applied with numerator the constant $1$ , and the domain it produces, the set where $x^{n}$ does not vanish, is exactly $R ∖ {0}$ ; no separate argument and no separate limit is needed. Rational exponents are a different matter, resting on Existence and uniqueness of $n$ -th roots: a unique $a^{1 / n} \geq 0$ with $(a^{1 / n})^{n} = a$ , and are treated on the companion page rather than here.
Claim 4 is a statement about a finite sum, not about an infinite one. Nothing here says anything about differentiating a series term by term; that is a separate question, needing hypotheses about convergence that this page does not have and does not assume.

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

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)$

Statement

Let $A, B \subseteq R$ , let $g : A \to R$ with $g [A] \subseteq B$ and let $f : B \to R$ , so that the composite $f \circ g : A \to R$ is defined. Let $c \in A$ be a limit point of $A$ (Limit point, isolated point, adherent point, derived set, and dense subset of $R$ ) at which $g$ is differentiable (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), put $b : = g (c)$ , and suppose $b$ is a limit point of $B$ at which $f$ is differentiable. Then $f \circ g$ is differentiable at $c$ and

$(f \circ g)^{'} (c) = f^{'} (g (c)) g^{'} (c) .$

Both limit-point hypotheses are needed, and neither is automatic. That $c$ is a limit point of $A$ is what makes $g^{'} (c)$ and $(f \circ g)^{'} (c)$ defined symbols; that $b = g (c)$ is a limit point of $B$ is what makes $f^{'} (b)$ one. Nothing forces the second: $g$ may be differentiable at $c$ and send $c$ to an isolated point of $B$ , and there $f^{'} (b)$ is not defined and the formula asserts nothing.

No case analysis appears anywhere. The naive difference-quotient proof writes $\frac{f (g (x)) - f (g (c))}{g (x) - g (c)} \cdot \frac{g (x) - g (c)}{x - c}$ and then has to say what happens where $g (x) = g (c)$ , which may occur at points arbitrarily close to $c$ . Carathéodory's factorisation never divides by the inner increment, so the difficulty does not arise.

Facts & Assumptions

Given: Sets $A, B \subseteq R$ , functions $g : A \to R$ with $g [A] \subseteq B$ and $f : B \to R$ , a point $c \in A$ that is a limit point of $A$ at which $g$ is differentiable, and the point $b : = g (c) \in B$ , a limit point of $B$ at which $f$ is differentiable (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, Limit point, isolated point, adherent point, derived set, and dense subset of $R$ ).

[L1]

Carathéodory's characterisation (Carathéodory's characterisation: $f$ is differentiable at $c$ if and only if there is $φ : A \to R$ , continuous at $c$ , with $f (x) - f (c) = φ (x) (x - c)$ for every $x \in A$ , and then $φ$ is unique and $φ (c) = f^{'} (c)$ ), used in both directions: for $D \subseteq R$ , a point $p \in D$ that is a limit point of $D$ and $h : D \to R$ , the function $h$ is differentiable at $p$ if and only if there is $η : D \to R$ , continuous at $p$ , with $h (y) - h (p) = η (y) (y - p)$ for every $y \in D$ , and then $η (p) = h^{'} (p)$ .

[L2]

[L3]

Composition of continuous functions (A composite of continuous functions is continuous, with no side hypothesis of the kind the composition of limits needs): if $g : A \to R$ has $g [A] \subseteq B$ and is continuous at $c \in A$ , and if $η : B \to R$ is continuous at $g (c)$ , then $η \circ g$ is continuous at $c$ (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).

[L4]

A function differentiable at a point is continuous there (A function differentiable at $c$ is continuous at $c$ ).

Proof

technique · direct

1.1

By [L1], applied to $g$ on $A$ at $c$ , fix $ψ : A \to R$ , continuous at $c$ , with $g (x) - g (c) = ψ (x) (x - c)$ for every $x \in A$ and $ψ (c) = g^{'} (c)$ .

L1choose

1.2

By [L1], applied to $f$ on $B$ at $b$ , fix $φ : B \to R$ , continuous at $b$ , with $f (y) - f (b) = φ (y) (y - b)$ for every $y \in B$ and $φ (b) = f^{'} (b)$ .

L1choose

2.1

The factorisation. Let $x \in A$ . Then $g (x) \in B$ , so taking $y : = g (x)$ in step 1.2 gives $f (g (x)) - f (b) = φ (g (x)) (g (x) - b)$ , and $g (x) - b = g (x) - g (c) = ψ (x) (x - c)$ by step 1.1. Since $(f \circ g) (c) = f (g (c)) = f (b)$ , this reads $(f \circ g) (x) - (f \circ g) (c) = χ (x) (x - c)$ for every $x \in A$ , where $χ : A \to R$ is the pointwise product $χ : = (φ \circ g) ψ$ .

step 1.1step 1.2

2.2

The outer factor is continuous at $c$ . By [L4] the function $g$ is continuous at $c$ ; by step 1.2 the function $φ$ is continuous at $b = g (c)$ ; and $g [A] \subseteq B$ . So $φ \circ g$ is continuous at $c$ by [L3].

step 1.2L3L4

3.1

The factor is continuous at $c$ , with the right value. $χ$ is the product of $φ \circ g$ , continuous at $c$ by step 2.2, with $ψ$ , continuous at $c$ by step 1.1, so $χ$ is continuous at $c$ by [L2]; and $χ (c) = φ (g (c)) ψ (c) = φ (b) ψ (c) = f^{'} (b) g^{'} (c)$ .

step 1.1step 2.2L2

4.1

By step 2.1 the function $χ : A \to R$ factors the increment of $f \circ g$ at $c$ , and by step 3.1 it is continuous at $c$ . So [L1], applied to $f \circ g$ on $A$ at the limit point $c$ , gives that $f \circ g$ is differentiable at $c$ with $(f \circ g)^{'} (c) = χ (c) = f^{'} (g (c)) g^{'} (c)$ .

step 2.1step 3.1L1∎

Remarks

Where the classical proof goes wrong, precisely. It divides by $g (x) - g (c)$ , which may vanish at points arbitrarily close to $c$ even when $g$ is differentiable at $c$ with $g^{'} (c) = 0$ ; the usual repair defines an auxiliary function equal to the outer quotient off the bad set and to $f^{'} (b)$ on it, and then proves that auxiliary function continuous. That auxiliary function is $φ \circ g$ , and Carathéodory's characterisation: $f$ is differentiable at $c$ if and only if there is $φ : A \to R$ , continuous at $c$ , with $f (x) - f (c) = φ (x) (x - c)$ for every $x \in A$ , and then $φ$ is unique and $φ (c) = f^{'} (c)$ is the observation that it exists before any repair is attempted.
What is composed is continuity, not differentiability. The only theorem about composites used above is A composite of continuous functions is continuous, with no side hypothesis of the kind the composition of limits needs, and it needs no side hypothesis, unlike the corresponding statement for limits. That is the whole reason the proof has no cases.
The formula is about the point $g (c)$ , not about $g$ near $c$ . Both derivatives on the right are taken at single points, and the theorem says nothing about $f$ on the image of any neighbourhood of $c$ . In particular no hypothesis is placed on $g [A]$ beyond its lying in $B$ .

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-28Open item page →

Derivative of an inverse: if $f$ is continuous and injective on a nondegenerate interval $I$ and differentiable at $c \in I$ with $f^{'} (c) \neq 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)$

Statement

Let $I \subseteq R$ be order-convex with at least two elements (Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length), let $f : I \to R$ be continuous on $I$ (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) and injective (Injection, surjection, bijection), and let $g : f [I] \to I$ be the inverse of $f : I \to f [I]$ supplied by Continuous inverse theorem: a continuous injective $f$ on an interval $I$ is a bijection onto the order-convex set $f [I]$ , and the inverse $g : f [I] \to I$ is continuous and strictly monotone in the same sense as $f$ . Let $c \in I$ and put $b : = f (c)$ .

Then $c$ is a limit point of $I$ and $b$ is a limit point of $f [I]$ , so that $f^{'} (c)$ and $g^{'} (b)$ are meaningful symbols (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), and, assuming $f$ is differentiable at $c$ :

if $f^{'} (c) \neq 0$ , then $g$ is differentiable at $b$ and $g^{'} (b) = \frac{1}{f^{'} (c)};$
if $f^{'} (c) = 0$ , then $g$ is not differentiable at $b$ .

The two claims together say that the inverse inherits differentiability exactly where the derivative does not vanish. Nothing is asserted at a point of $f [I]$ that is not of the form $f (c)$ with $f$ differentiable at $c$ , and nothing is asserted about $g$ being differentiable on a set.

No compactness and no boundedness is assumed. $I$ may be open, half-open or unbounded; all that is used of it is order-convexity and the presence of two distinct points, the latter being exactly what makes every point of $I$ a limit point of $I$ (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).

Facts & Assumptions

Given: An order-convex $I \subseteq R$ with at least two elements, a continuous injective $f : I \to R$ , a point $c \in I$ , and $b : = f (c)$ ; from step 1.3 onwards also the hypothesis that $f$ is differentiable at $c$ (Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length, 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, Injection, surjection, bijection, 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).

[L1]

Continuous inverse theorem (Continuous inverse theorem: a continuous injective $f$ on an interval $I$ is a bijection onto the order-convex set $f [I]$ , and the inverse $g : f [I] \to I$ is continuous and strictly monotone in the same sense as $f$ , claims 2, 3 and 5): $f [I]$ is order-convex; $f : I \to f [I]$ is a bijection, so there is exactly one $g : f [I] \to I$ with $g (f (x)) = x$ for every $x \in I$ and $f (g (u)) = u$ for every $u \in f [I]$ ; and $g$ is continuous on $f [I]$ .

[L2]

Carathéodory's characterisation (Carathéodory's characterisation: $f$ is differentiable at $c$ if and only if there is $φ : A \to R$ , continuous at $c$ , with $f (x) - f (c) = φ (x) (x - c)$ for every $x \in A$ , and then $φ$ is unique and $φ (c) = f^{'} (c)$ ), used in both directions: for $D \subseteq R$ , a point $p \in D$ that is a limit point of $D$ and $h : D \to R$ , the function $h$ is differentiable at $p$ if and only if there is $η : D \to R$ , continuous at $p$ , with $h (y) - h (p) = η (y) (y - p)$ for every $y \in D$ , and then $η (p) = h^{'} (p)$ .

[L3]

Every point of an order-convex subset of $R$ with at least two elements is a limit point of that set (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, Limit point, isolated point, adherent point, derived set, and dense subset of $R$ ).

[L4]

Injectivity (Injection, surjection, bijection): $f (x) = f (x^{'})$ implies $x = x^{'}$ , so $x \neq c$ gives $f (x) \neq f (c)$ ; and the image $f [I] = {f (x) : x \in I}$ .

[L5]

Algebra and composition of continuous functions: a composite of functions continuous at the relevant points is continuous (A composite of continuous functions is continuous, with no side hypothesis of the kind the composition of limits needs); every constant function is continuous (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 5); and if $u, v : D \to R$ are continuous at $p \in D$ with $v (p) \neq 0$ , then $(u / v)$ restricted to ${y \in D : v (y) \neq 0}$ is continuous at $p$ (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 4).

[L6]

Chain rule (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)$ ): with $g$ differentiable at the limit point $b = f (c)$ of $f [I]$ and $f$ differentiable at the limit point $c$ of $I$ , the composite $g \circ f$ is differentiable at $c$ with $(g \circ f)^{'} (c) = g^{'} (b) f^{'} (c)$ .

[L7]

The identity on a set $D$ is differentiable at every limit point $p$ of $D$ with derivative $1$ : its difference quotient is $(y - p) / (y - p) = 1$ for every $y \in D ∖ {p}$ , a constant function, whose limit at $p$ is $1$ (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, The $ε$ - $δ$ limit $\lim_{x \to c} f (x) = L$ of $f : A \to R$ at a limit point $c$ of $A$ ). The derivative at a point is a single real (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), and $0 \neq 1$ in $R$ (The multiplicative identity is positive).

Proof

technique · direct

1.1

$I$ has at least two elements, so by [L4] its image $f [I]$ has at least two elements; and $f [I]$ is order-convex by [L1]. So [L3] applies to both sets: every point of $I$ is a limit point of $I$ , and every point of $f [I]$ is a limit point of $f [I]$ . In particular $c$ is a limit point of $I$ and $b = f (c) \in f [I]$ is a limit point of $f [I]$ .

L1L3L4

1.2

Fix the inverse $g : f [I] \to I$ of $f : I \to f [I]$ , continuous on $f [I]$ ; it satisfies $g (f (x)) = x$ for every $x \in I$ , so in particular $g (b) = c$ .

L1choose

1.3

Assume $f$ is differentiable at $c$ . By [L2], applied to $f$ on $I$ at the limit point $c$ , fix $φ : I \to R$ , continuous at $c$ , with $f (x) - f (c) = φ (x) (x - c)$ for every $x \in I$ and $φ (c) = f^{'} (c)$ .

L2choose

2.1

$φ (x) \neq 0$ for every $x \in I$ with $x \neq c$ : injectivity gives $f (x) \neq f (c)$ , so $φ (x) (x - c) \neq 0$ and hence $φ (x) \neq 0$ . If moreover $f^{'} (c) \neq 0$ then $φ (c) = f^{'} (c) \neq 0$ as well, so $φ$ vanishes at no point of $I$ .

step 1.3L4

2.2

The increment of $g$ , rewritten. Let $u \in f [I]$ and put $x : = g (u) \in I$ , so $f (x) = u$ by [L1]. Then $u - b = f (x) - f (c) = φ (x) (x - c) = φ (g (u)) (g (u) - g (b))$ , using $g (b) = c$ from step 1.2.

step 1.2step 1.3L1

2.3

Claim 2. Assume $f^{'} (c) = 0$ , and suppose $g$ were differentiable at $b$ . Since $f [I] \subseteq f [I]$ , since $f$ is differentiable at the limit point $c$ of $I$ and since $b = f (c)$ is a limit point of $f [I]$ by step 1.1, the chain rule [L6] gives that $g \circ f : I \to R$ is differentiable at $c$ with $(g \circ f)^{'} (c) = g^{'} (b) f^{'} (c) = g^{'} (b) \cdot 0 = 0$ . But $g \circ f$ is the identity on $I$ by step 1.2, and by [L7] the identity on $I$ is differentiable at the limit point $c$ with derivative $1$ ; the derivative at $c$ being a single real, this forces $0 = 1$ , which [L7] excludes. So $g$ is not differentiable at $b$ .

step 1.1step 1.2L6L7

3.1

The reciprocal factor. Assume $f^{'} (c) \neq 0$ . The map $g$ is continuous at $b$ by step 1.2 and sends $f [I]$ into $I$ , and $φ$ is continuous at $c = g (b)$ by step 1.3, so $φ \circ g : f [I] \to R$ is continuous at $b$ by [L5]; by step 2.1 it vanishes at no point of $f [I]$ , since $g$ takes values in $I$ , and $(φ \circ g) (b) = φ (c) = f^{'} (c) \neq 0$ . Hence, by [L5] applied with the constant numerator $1$ and denominator $φ \circ g$ on the domain $f [I]$ , where the set on which the denominator does not vanish is the whole of $f [I]$ , the function $Φ : = 1 / (φ \circ g) : f [I] \to R$ is continuous at $b$ and $Φ (b) = 1 / f^{'} (c)$ .

step 1.2step 1.3step 2.1L5

4.1

The factorisation for $g$ . Assume $f^{'} (c) \neq 0$ and let $u \in f [I]$ . Dividing the identity of step 2.2 by the nonzero number $(φ \circ g) (u)$ gives $g (u) - g (b) = Φ (u) (u - b)$ , and this holds for every $u \in f [I]$ .

step 2.2step 3.1

5.1

Claim 1. Assume $f^{'} (c) \neq 0$ . By step 1.1 the point $b$ is a limit point of $f [I]$ ; by step 4.1 the function $Φ : f [I] \to R$ factors the increment of $g$ at $b$ ; and by step 3.1 it is continuous at $b$ . So [L2], applied to $g$ on $f [I]$ at $b$ , gives that $g$ is differentiable at $b$ with $g^{'} (b) = Φ (b) = 1 / f^{'} (c)$ .

step 1.1step 3.1step 4.1L2

6.1

Claim 1 is step 5.1 and claim 2 is step 2.3, and the two limit-point assertions are step 1.1.

step 2.3step 5.1∎

Remarks

Why claim 2 is not a defect of the method. It is a theorem: at a point where $f^{'} = 0$ no inverse can be differentiable, because the chain rule would then make the derivative of the identity equal to $0$ . The geometry is the familiar one, a horizontal tangent reflecting into a vertical one, and the argument above is that picture with no picture in it.
What is used of Continuous inverse theorem: a continuous injective $f$ on an interval $I$ is a bijection onto the order-convex set $f [I]$ , and the inverse $g : f [I] \to I$ is continuous and strictly monotone in the same sense as $f$ , and what is not. Only that $f [I]$ is order-convex, that the two-sided inverse exists and is unique, and that it is continuous. The strict monotonicity that theorem also proves is not needed here, though it is what makes the situation intelligible.
The formula is often written $g^{'} (b) = 1 / f^{'} (g (b))$ , which is the same statement since $g (b) = c$ . Written that way it is a formula for $g^{'}$ at every point of $f [I]$ at which the hypothesis holds, and that is how the companion page uses it to differentiate $x \mapsto x^{1 / n}$ .

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (z-ai/glm-5.2)audited 2026-07-28Open item page →

Local (relative) maximum and minimum of $f : A \to R$ at a point, the strict forms, and what it means for the point to be interior to $A$

Definition

Throughout, $R$ is the complete ordered field (Complete ordered field (least-upper-bound property)) and neighbourhoods are those of The $ε$ -neighbourhood and the punctured $ε$ -neighbourhood of a point of $R$ . Let $A \subseteq R$ , let $f : A \to R$ and let $c \in A$ .

$f$ has a local maximum at $c$ , also called a relative maximum, when there is a real $ε > 0$ with $f (x) \leq f (c) for every x \in A \cap N_{ε} (c) .$
$f$ has a local minimum at $c$ when there is a real $ε > 0$ with $f (x) \geq f (c)$ for every $x \in A \cap N_{ε} (c)$ .
$f$ has a local extremum at $c$ when it has a local maximum or a local minimum at $c$ .
$f$ has a strict local maximum at $c$ when there is a real $ε > 0$ with $f (x) < f (c)$ for every $x \in A \cap N_{ε}^{*} (c)$ , the neighbourhood being punctured; and a strict local minimum at $c$ when $f (x) > f (c)$ for every such $x$ .

The point $c$ is interior to $A$ when $c \in A^{\circ}$ (Interior, closure, boundary and exterior of a subset of $R$ ), equivalently when there is a real $ε > 0$ with $N_{ε} (c) \subseteq A$ ; that equivalence is the pointwise description of the interior proved in Interior, closure, boundary and exterior of a subset of $R$ and is not reproved here.

The strict forms must puncture, and the weak forms must not. With an unpunctured neighbourhood the strict condition would read $f (c) < f (c)$ at $x = c$ , which no function satisfies, so the notion would be empty. With a punctured neighbourhood the weak condition would say nothing at $c$ , which is harmless but pointless, since $f (c) \leq f (c)$ holds anyway. So each form is stated with the quantifier that makes it a condition.

Four consequences, each an obligation this definition carries.

The condition does not depend on which witness $ε$ is produced. If it holds for $ε$ , it holds for every real $ε^{'}$ with $0 < ε^{'} \leq ε$ , because $N_{ε^{'}} (c) \subseteq N_{ε} (c)$ (The $ε$ -neighbourhood and the punctured $ε$ -neighbourhood of a point of $R$ ). So the existential quantifier may be read as "for all sufficiently small $ε$ ", and two witnesses can always be replaced by the smaller of them.
A local maximum really is a maximum, of a set. $f$ has a local maximum at $c$ exactly when there is a real $ε > 0$ with $f (c) = \max f [A \cap N_{ε} (c)]$ (Maximum and minimum of a set). Indeed $c \in A \cap N_{ε} (c)$ , since $c \in A$ and $∣ c - c ∣ = 0 < ε$ (The $ε$ -neighbourhood and the punctured $ε$ -neighbourhood of a point of $R$ ), so $f (c)$ belongs to that image; and the defining inequality says exactly that $f (c)$ bounds the image above. Conversely a maximum of the image is an element of it bounding it above, which is the defining inequality. The same argument with the order reversed identifies a local minimum with a minimum of the same image.
A strict local extremum is a local extremum. If $f (x) < f (c)$ for every $x \in A \cap N_{ε}^{*} (c)$ , then $f (x) \leq f (c)$ for every $x \in A \cap N_{ε} (c)$ : the points of the unpunctured neighbourhood other than $c$ are covered by the hypothesis, and at $x = c$ the inequality $f (c) \leq f (c)$ is automatic.
A global extremum is a local one. If $f (c) = \max f [A]$ then $f$ has a local maximum at $c$ , with $ε : = 1$ serving, since $A \cap N_{1} (c) \subseteq A$ ; and dually for the minimum.

An interior point of $A$ is a limit point of $A$ . Suppose $N_{ε} (c) \subseteq A$ with $ε > 0$ real, and let a real $δ > 0$ be given. The punctured neighbourhood $N_{ρ}^{*} (c)$ with $ρ : = \min {δ, ε} > 0$ is nonempty (The $ε$ -neighbourhood and the punctured $ε$ -neighbourhood of a point of $R$ ) and is contained both in $N_{δ}^{*} (c)$ and in $N_{ε} (c) \subseteq A$ ; so $N_{δ}^{*} (c) \cap A \neq \emptyset$ . As $δ$ was arbitrary, $c$ is a limit point of $A$ (Limit point, isolated point, adherent point, derived set, and dense subset of $R$ ). This is what makes an interior extremum a place where a derivative can be spoken of at all, and it is the reason the interiority hypothesis appears in Fermat's theorem below rather than being replaced by something weaker.

Remarks

"The local maximum" is not a legitimate phrase. A function may have local maxima at many points, and the definite article belongs only to the value $f (c)$ once the point $c$ is fixed. A global maximum value is unique when it exists (Maximum and minimum of a set); a local one is not, and neither is the point.
Local is a statement about $A$ , not about $R$ . The comparison runs over $A \cap N_{ε} (c)$ , so a function on a small domain has local maxima easily: every point of $A$ at which $A \cap N_{ε} (c) = {c}$ for some $ε$ , that is every isolated point of $A$ (Limit point, isolated point, adherent point, derived set, and dense subset of $R$ ), carries both a strict local maximum and a strict local minimum, the punctured condition being vacuous there. Interiority is the hypothesis that rules that degenerate case out.
Endpoints are the case to keep in mind. For $A = [a, b]$ with $a < b$ (Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length) the points $a$ and $b$ are not interior to $A$ : any $N_{ε} (a)$ contains $a - ε / 2$ , which is not in $[a, b]$ . A function may perfectly well attain its greatest value there, with no vanishing derivative anywhere, and the companion page works that case out.
Nothing here mentions a derivative. The definition is purely about the order, and it applies to functions that are nowhere differentiable. What the next items add is the interaction, in one direction only: differentiability at an interior extremum forces the derivative to vanish, and the converse is false.

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

Fermat's interior extremum theorem: if $f$ has a local extremum at a point $c$ interior to its domain and is differentiable at $c$ , then $f^{'} (c) = 0$

Statement

Let $A \subseteq R$ , let $f : A \to R$ and let $c \in A$ be interior to $A$ (Local (relative) maximum and minimum of $f : A \to R$ at a point, the strict forms, and what it means for the point to be interior to $A$ , Interior, closure, boundary and exterior of a subset of $R$ ). Suppose $f$ has a local extremum at $c$ (Local (relative) maximum and minimum of $f : A \to R$ at a point, the strict forms, and what it means for the point to be interior to $A$ ) and is differentiable at $c$ (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

$f^{'} (c) = 0.$

The symbol $f^{'} (c)$ is meaningful under these hypotheses because an interior point of $A$ is a limit point of $A$ , which is proved in Local (relative) maximum and minimum of $f : A \to R$ at a point, the strict forms, and what it means for the point to be interior to $A$ .

Interiority is a hypothesis and not a convenience. At a point of $A$ that is not interior, the argument below cannot place points of $A$ on both sides of $c$ , and the conclusion genuinely fails: the companion page exhibits a function on $[0, 1]$ attaining both its greatest and its least value at points where the derivative is $1$ .

No converse is asserted. A vanishing derivative does not produce an extremum. The witness is the cubic of FALSE: if $f^{'} (c) = 0$ then $f$ is not increasing on any interval containing $c$ , which has $f^{'} (0) = 0$ and neither a local maximum nor a local minimum at $0$ ; that failure is recorded in the remarks of that item, not as an item of its own.

Facts & Assumptions

Given: A set $A \subseteq R$ , a function $f : A \to R$ and a point $c \in A$ interior to $A$ , at which $f$ has a local extremum and is differentiable (Local (relative) maximum and minimum of $f : A \to R$ at a point, the strict forms, and what it means for the point to be interior to $A$ , 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).

[A1]

$c$ is interior to $A$ : there is a real $ε_{A} > 0$ with $N_{ε_{A}} (c) \subseteq A$ ; and such a $c$ is a limit point of $A$ , so $f^{'} (c)$ is defined (Local (relative) maximum and minimum of $f : A \to R$ at a point, the strict forms, and what it means for the point to be interior to $A$ , Interior, closure, boundary and exterior of a subset of $R$ , Limit point, isolated point, adherent point, derived set, and dense subset of $R$ ).

[A2]

$f$ has a local extremum at $c$ : there is a real $ρ > 0$ such that either $f (x) \leq f (c)$ for every $x \in A \cap N_{ρ} (c)$ , or $f (x) \geq f (c)$ for every $x \in A \cap N_{ρ} (c)$ (Local (relative) maximum and minimum of $f : A \to R$ at a point, the strict forms, and what it means for the point to be interior to $A$ ).

[L1]

Derivative (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): the difference quotient $q (x) : = (f (x) - f (c)) / (x - c)$ is a function on $A ∖ {c}$ , the point $c$ is a limit point of $A ∖ {c}$ , and $\lim_{x \to c} q (x) = f^{'} (c)$ (The $ε$ - $δ$ limit $\lim_{x \to c} f (x) = L$ of $f : A \to R$ at a limit point $c$ of $A$ ). In particular $f (x) - f (c) = q (x) (x - c)$ for every $x \in A$ with $x \neq c$ .

[L2]

Sign preservation (If $\lim_{x \to c} f (x) = L \neq 0$ then $∣ f ∣ > ∣ L ∣ / 2$ on a punctured neighbourhood of $c$ ; in particular if $L > 0$ then $f > L / 2 > 0$ there): if $h$ is a function on a set $D$ having $c$ as a limit point and $\lim_{x \to c} h (x) = L$ with $L \neq 0$ , then there is a real $δ > 0$ such that every $x \in D$ with $0 < ∣ x - c ∣ < δ$ satisfies $h (x) > L / 2 > 0$ when $L > 0$ , and $h (x) < L / 2 < 0$ when $L < 0$ .

[L3]

Neighbourhoods (The $ε$ -neighbourhood and the punctured $ε$ -neighbourhood of a point of $R$ ): $N_{ε} (c) = {y : ∣ y - c ∣ < ε}$ , and of finitely many positive reals the smallest is positive.

[L4]

Order arithmetic (Sign rules for products and monotonicity of multiplication, Ordered field): a product of two positive reals is positive, a product of a positive and a negative real is negative, and trichotomy, so $f^{'} (c) \neq 0$ means $f^{'} (c) > 0$ or $f^{'} (c) < 0$ , exclusively.

Proof

technique · contradiction

1.1

Suppose, for contradiction, that $f^{'} (c) \neq 0$ ; by trichotomy either $f^{'} (c) > 0$ or $f^{'} (c) < 0$ .

assume-contraL4

1.2

Fix a real $ε_{A} > 0$ with $N_{ε_{A}} (c) \subseteq A$ .

A1choose

1.3

Fix a real $ρ > 0$ as in [A2], so that on $A \cap N_{ρ} (c)$ the function $f$ never exceeds $f (c)$ , or never falls below it.

A2choose

2.1

Apply [L2] to $h : = q$ on the domain $D : = A ∖ {c}$ , of which $c$ is a limit point by [L1], with $L : = f^{'} (c) \neq 0$ : fix a real $δ > 0$ such that every $x \in A$ with $0 < ∣ x - c ∣ < δ$ satisfies $q (x) > f^{'} (c) / 2 > 0$ if $f^{'} (c) > 0$ , and $q (x) < f^{'} (c) / 2 < 0$ if $f^{'} (c) < 0$ . The clause $0 < ∣ x - c ∣$ makes the two descriptions of the range of $x$ , over $A$ and over $A ∖ {c}$ , the same.

step 1.1L1L2choose

3.1

Put $η : = \min {ε_{A}, ρ, δ}$ , a positive real, and set $x_{+} : = c + η / 2$ and $x_{-} : = c - η / 2$ . Each satisfies $∣ x_{\pm} - c ∣ = η / 2 < η$ , so each lies in $N_{ε_{A}} (c) \subseteq A$ , each lies in $N_{ρ} (c)$ , and each satisfies $0 < ∣ x_{\pm} - c ∣ < δ$ . In particular $x_{+}, x_{-} \in A \cap N_{ρ} (c)$ and both differ from $c$ .

step 1.2step 1.3step 2.1L3

4.1

Suppose $f^{'} (c) > 0$ . By step 2.1, $q (x_{+}) > 0$ and $q (x_{-}) > 0$ . Since $x_{+} - c = η / 2 > 0$ , [L1] and [L4] give $f (x_{+}) - f (c) = q (x_{+}) (x_{+} - c) > 0$ ; since $x_{-} - c = - η / 2 < 0$ , they give $f (x_{-}) - f (c) = q (x_{-}) (x_{-} - c) < 0$ . So $f (x_{+}) > f (c)$ and $f (x_{-}) < f (c)$ .

step 2.1step 3.1L1L4

4.2

Suppose instead $f^{'} (c) < 0$ . By step 2.1, $q (x_{+}) < 0$ and $q (x_{-}) < 0$ . The same two products, with the signs of the quotients reversed, give $f (x_{+}) - f (c) < 0$ and $f (x_{-}) - f (c) > 0$ . So $f (x_{-}) > f (c)$ and $f (x_{+}) < f (c)$ .

step 2.1step 3.1L1L4

5.1

In both cases of step 1.1 there is a point of $A \cap N_{ρ} (c)$ at which $f$ takes a value strictly greater than $f (c)$ , and a point of $A \cap N_{ρ} (c)$ at which it takes a value strictly smaller: the two points are $x_{+}$ and $x_{-}$ in one order or the other, and both lie in $A \cap N_{ρ} (c)$ by step 3.1.

step 3.1step 4.1step 4.2L4

6.1

By step 1.3 one of two things holds on $A \cap N_{ρ} (c)$ : either no value exceeds $f (c)$ , or none falls below it. Step 5.1 produces a value of each kind, so both alternatives fail, and [A2] guarantees that one of them holds. The assumption of step 1.1 is therefore untenable, and $f^{'} (c) = 0$ .

step 1.3step 5.1A2discharge-contradiction∎

Remarks

What the proof actually uses. Only that the difference quotient keeps the sign of its limit near $c$ , and that $c$ has points of $A$ on both sides of it arbitrarily close. The first is If $\lim_{x \to c} f (x) = L \neq 0$ then $∣ f ∣ > ∣ L ∣ / 2$ on a punctured neighbourhood of $c$ ; in particular if $L > 0$ then $f > L / 2 > 0$ there; the second is exactly what interiority buys, and it is where the hypothesis is spent. No continuity of $f$ away from $c$ , and no hypothesis on $A$ beyond containing a neighbourhood of $c$ , is needed.
The one-sided reading. At a point $c$ with points of $A$ on one side only, the argument still gives half of the conclusion: if $f$ has a local maximum there and only points to the right, then $f^{'} (c) \leq 0$ . This page does not state that refinement, because it does not use it, and the companion page's witness at an endpoint is the same observation seen from outside (The identity on $[0, 1]$ attains its maximum at $1$ and its minimum at $0$ with derivative $1$ at both, so Fermat's theorem genuinely needs the extremum to be at an interior point ↗).
A stationary point is not an extremum. The converse of this theorem is false, and the standard witness, $x \mapsto x^{3}$ at $0$ , is the same function that this page uses to refute a different plausible claim about vanishing derivatives.

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

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)$

Statement

Let $a, b \in R$ with $a < b$ , let $f : [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 a function 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), and suppose

$f (a) = f (b) .$

Then there is $c \in (a, b)$ with $f^{'} (c) = 0$ .

Three hypotheses, three different jobs. Continuity on the closed interval is what the extreme value theorem consumes; differentiability on the open interval is what Fermat's theorem consumes, and it is asked for nowhere else; and $f (a) = f (b)$ is what forces the extremum inside when neither extremum is attained in the interior. Continuity at the two endpoints cannot be dropped, and a false statement later on this page records a witness for that.

Differentiability is meant with respect to the domain $[a, b]$ . For $c$ in the open interval that is the same condition as differentiability of any restriction of $f$ to a subinterval around $c$ , since only points near $c$ enter, but the phrase is fixed here so that the citation of Fermat's interior extremum theorem: if $f$ has a local extremum at a point $c$ interior to its domain and is differentiable at $c$ , then $f^{'} (c) = 0$ , whose hypothesis is interiority in the domain, is exact.

Facts & Assumptions

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

[L1]

$[a, b]$ is closed (Open subset of $R$ (every point has a neighbourhood inside it), closed subset (complement open), and clopen) and bounded (Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length, Lower bound, bounded below, bounded set), hence compact (A subset of $R$ is compact if and only if it is closed and bounded, Open cover, subcover, compact subset of $R$ (every open cover has a finite subcover), and sequentially compact subset); and it is nonempty, since $a \leq a \leq b$ gives $a \in [a, b]$ .

[L2]

Extreme value theorem (Extreme value theorem: a continuous real function on a nonempty compact subset of $R$ attains a greatest and a least value): for $f$ continuous on $A$ and $K \subseteq A$ nonempty and compact there are $p, q \in K$ with $f (q) \leq f (x) \leq f (p)$ for every $x \in K$ , so that $f (p) = \max f [K]$ and $f (q) = \min f [K]$ (Maximum and minimum of a set).

[L3]

Every point of $(a, b)$ is interior to $[a, b]$ : for $c$ with $a < c < b$ put $ε : = \min {c - a, b - c}$ , a positive real; every $y$ with $∣ y - c ∣ < ε$ satisfies $y > c - ε \geq a$ and $y < c + ε \leq b$ , so $N_{ε} (c) \subseteq (a, b) \subseteq [a, b]$ (The $ε$ -neighbourhood and the punctured $ε$ -neighbourhood of a point of $R$ , Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length, Interior, closure, boundary and exterior of a subset of $R$ ).

[L4]

A value $f (c)$ that is a greatest value of $f$ over the whole of its domain is a local maximum at $c$ , and a least value is a local minimum at $c$ (Local (relative) maximum and minimum of $f : A \to R$ at a point, the strict forms, and what it means for the point to be interior to $A$ , claim 4 of its body).

[L5]

Fermat's interior extremum theorem (Fermat's interior extremum theorem: if $f$ has a local extremum at a point $c$ interior to its domain and is differentiable at $c$ , then $f^{'} (c) = 0$ ): a local extremum at a point interior to the domain, at which the function is differentiable, forces the derivative there to vanish.

[L6]

$(a, b)$ is nonempty when $a < b$ , since $a < (a + b) / 2 < b$ (Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length).

[L7]

A constant function $h$ on $[a, b]$ is differentiable at every point $c$ of $[a, b]$ with $h^{'} (c) = 0$ : every point of the nondegenerate order-convex set $[a, b]$ is a limit point of it, and the difference quotient of $h$ at $c$ is the constant $0$ on $[a, b] ∖ {c}$ , whose limit at $c$ is $0$ (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, The $ε$ - $δ$ limit $\lim_{x \to c} f (x) = L$ of $f : A \to R$ at a limit point $c$ of $A$ ).

Proof

technique · direct

1.1

The set $[a, b]$ is nonempty and compact, and $f$ is continuous on it.

1.2

Since $a < b$ , the open interval $(a, b)$ is nonempty; fix $m : = (a + b) / 2 \in (a, b)$ .

L6choose

2.1

By [L2], applied with $A : = K : = [a, b]$ , fix $p, q \in [a, b]$ with $f (q) \leq f (x) \leq f (p)$ for every $x \in [a, b]$ .

step 1.1L2choose

3.1

Case A: at least one of $p, q$ lies in $(a, b)$ . Fix such a point and call it $c$ . By [L3] the point $c$ is interior to $[a, b]$ , and $f$ is differentiable at $c$ because $c \in (a, b)$ . By step 2.1 and [L4], $f$ has a local maximum at $c$ if $c$ is the point $p$ , and a local minimum at $c$ if it is the point $q$ ; either way a local extremum. So [L5] gives $f^{'} (c) = 0$ , and $c \in (a, b)$ .

step 2.1L3L4L5

3.2

Case B: neither $p$ nor $q$ lies in $(a, b)$ . A point of $[a, b]$ outside $(a, b)$ satisfies $a \leq x \leq b$ and not $a < x < b$ , hence equals $a$ or $b$ ; so $p, q \in {a, b}$ and, since $f (a) = f (b)$ , both $f (p)$ and $f (q)$ equal $f (a)$ . By step 2.1, every $x \in [a, b]$ satisfies $f (a) = f (q) \leq f (x) \leq f (p) = f (a)$ , so $f (x) = f (a)$ . Thus $f$ is the constant function with value $f (a)$ on $[a, b]$ .

step 2.1

4.1

In case B, [L7] gives that $f$ is differentiable at every point of $[a, b]$ with derivative $0$ ; in particular $f^{'} (m) = 0$ , and $m \in (a, b)$ by step 1.2.

step 1.2step 3.2L7

5.1

The two cases are exhaustive, since either at least one of $p, q$ lies in $(a, b)$ or neither does. Case A supplies a point $c \in (a, b)$ with $f^{'} (c) = 0$ by step 3.1, and case B supplies the point $m$ by step 4.1.

step 3.1step 4.1∎

Remarks

The constant case is not a degenerate nuisance, it is the case where the extremum sits on the boundary. When $f$ is constant the greatest and least values are attained at the endpoints as well as everywhere else, so nothing forces the extreme value theorem to hand back an interior point; the argument has to produce a point of $(a, b)$ by hand, and any point will do.
Why compactness enters at all. Only through Extreme value theorem: a continuous real function on a nonempty compact subset of $R$ attains a greatest and a least value, and only to know that the greatest and least values are attained. A supremum that is not attained is useless here: Fermat's theorem is a statement about a point, not about a bound. That is precisely the hypothesis the companion page's witness removes.
Nothing is claimed about how many such $c$ there are, or where. A single $c$ is produced, and the proof gives no way to locate it; the theorem is an existence statement and is used only as one.

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

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]

[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 ↗.

CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-28Open item page →

The mean value theorem, as the case $g (x) = x$ of Cauchy's: for $f$ continuous on $[a, b]$ with $a < b$ and differentiable on $(a, b)$ there is $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$

Statement

Let $a, b \in R$ with $a < b$ and let $f : [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 a function 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) = f^{'} (c) (b - a) .$

Equivalently, since $b - a \neq 0$ , there is $c \in (a, b)$ at which $f^{'} (c) = (f (b) - f (a)) / (b - a)$ : the derivative somewhere inside equals the average rate of change across the whole interval.

Continuity on the closed interval cannot be dropped. Differentiability at every point of $(a, b)$ alone does not suffice: a function on $[0, 1]$ , differentiable at every point of $(0, 1)$ with derivative constantly $1$ , for which no $c$ works, is exhibited later on this page as a false statement, and the companion page works the same witness out in full.

Facts & Assumptions

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

[L1]

Cauchy's mean value theorem (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): for $f, g$ continuous on $[a, b]$ and differentiable at every point of $(a, b)$ there is $c \in (a, b)$ with $(f (b) - f (a)) g^{'} (c) = (g (b) - g (a)) f^{'} (c)$ .

[L2]

The identity $x \mapsto x$ is continuous at every point of any $A \subseteq R$ (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 5).

[L3]

The identity $g$ on $[a, b]$ is differentiable at every $c \in [a, b]$ with $g^{'} (c) = 1$ : with $a < b$ the set $[a, b]$ is order-convex with at least two elements, so every one of its points is a limit point of it (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); and the difference quotient of $g$ at $c$ is $(x - c) / (x - c) = 1$ for every $x \in [a, b]$ with $x \neq c$ , a constant function, whose limit at $c$ is $1$ (The $ε$ - $δ$ limit $\lim_{x \to c} f (x) = L$ of $f : A \to R$ at a limit point $c$ of $A$ , 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).

Proof

technique · direct

1.1

Define $g : [a, b] \to R$ by $g (x) : = x$ .

construct

2.1

$g$ is continuous on $[a, b]$ by [L2]; it is differentiable at every $c \in (a, b)$ with $g^{'} (c) = 1$ by [L3]; and $g (b) - g (a) = b - a$ .

step 1.1L2L3

3.1

By step 2.1 the pair $f, g$ satisfies every hypothesis of [L1], so there is $c \in (a, b)$ with $(f (b) - f (a)) g^{'} (c) = (g (b) - g (a)) f^{'} (c)$ . Substituting $g^{'} (c) = 1$ and $g (b) - g (a) = b - a$ gives $f (b) - f (a) = f^{'} (c) (b - a)$ .

step 2.1L1∎

Remarks

The geometric reading, and what it is not. The conclusion says that some tangent line is parallel to the chord from $(a, f (a))$ to $(b, f (b))$ . It does not say which one, it does not say there is only one, and it says nothing at all about $f$ between the endpoints beyond the hypotheses. Every use of the theorem on this page is a use of the equation, never of the picture.
Why this is a corollary and not the primitive statement. 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 is proved from 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)$ with one auxiliary function, and this statement is that theorem at $g (x) = x$ ; deriving it the other way round, from this statement to Cauchy's, is also possible but needs an auxiliary function of its own, so nothing is saved. What matters is that both rest on Rolle, and Rolle on the extreme value theorem.
The two hypotheses are on different sets on purpose. Continuity is asked for on the closed interval and differentiability only on the open one, so nothing at all is required of the difference quotients at $a$ and at $b$ . Weakening the continuity in step with the differentiability, so that both are asked for on $(a, b)$ only, destroys the theorem, which is exactly what $f (x) = x$ on $[0, 1)$ with $f (1) = 0$ is differentiable at every point of $(0, 1)$ with $f^{'} \equiv 1$ , yet no $c$ satisfies $f (1) - f (0) = f^{'} (c)$ , so continuity on the closed interval cannot be dropped from the mean value theorem ↗ shows on the companion page.

CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-28Open item page →

A function continuous on an interval $I$ whose derivative vanishes at every interior point of $I$ is constant on $I$ ; consequently two such functions with the same derivative differ by a constant

Statement

Let $I \subseteq R$ be order-convex (Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length) and let $f : I \to R$ be continuous on $I$ (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) and differentiable at every point of $I$ that is interior to $I$ (Interior, closure, boundary and exterior of a subset of $R$ , 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), with

$f^{'} (x) = 0 at every interior point x of I .$

Then $f$ is constant on $I$ : there is a real $k$ with $f (x) = k$ for every $x \in I$ .

Consequently, if $f, g : I \to R$ are both continuous on $I$ and both differentiable at every interior point of $I$ , with $f^{'} (x) = g^{'} (x)$ at every interior point $x$ , then there is a real $k$ with

$f (x) = g (x) + k for every x \in I .$

Order-convexity of $I$ is essential and is not a convenience. The conclusion is false on a domain that falls into separate pieces, since a function may be constant on each piece with different constants; nothing in the proof would survive, because the mean value theorem is applied to the segment joining two points of the domain and that segment must lie in the domain.

The hypothesis is imposed only at interior points. At an endpoint of $I$ nothing is asked at all: $f$ need not be differentiable there, and the proof never evaluates a difference quotient at an endpoint, since it applies the mean value theorem on a segment $[u, v] \subseteq I$ and uses the derivative only at points of $(u, v)$ , all of which are interior to $I$ . What is not meant is that the derivative at an endpoint is free to be nonzero: once $f$ is known to be constant its difference quotient at an endpoint is constantly $0$ , so wherever $f^{'}$ exists at an endpoint it is $0$ too. That is a consequence of the theorem, not a hypothesis of it.

Facts & Assumptions

Given: An order-convex $I \subseteq R$ and a function $f : I \to R$ , continuous on $I$ and differentiable with vanishing derivative at every interior point of $I$ ; for the second claim also a second such function $g$ with $f^{'} = g^{'}$ at every interior point.

[L1]

Mean value theorem (The mean value theorem, as the case $g (x) = x$ of Cauchy's: for $f$ continuous on $[a, b]$ with $a < b$ and differentiable on $(a, b)$ there is $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$ ): for $u < v$ and $h : [u, v] \to R$ continuous on $[u, v]$ and differentiable at every point of $(u, v)$ , there is $c \in (u, v)$ with $h (v) - h (u) = h^{'} (c) (v - u)$ .

[L2]

Order-convexity (Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length): if $u, v \in I$ and $u \leq z \leq v$ then $z \in I$ ; so $u, v \in I$ with $u \leq v$ gives $[u, v] \subseteq I$ .

[L3]

For $u < v$ in $I$ and $x \in (u, v)$ , the point $x$ is interior to $I$ : put $ε : = \min {x - u, v - x}$ , a positive real; every $y$ with $∣ y - x ∣ < ε$ satisfies $u < y < v$ , so $N_{ε} (x) \subseteq (u, v) \subseteq [u, v] \subseteq I$ (The $ε$ -neighbourhood and the punctured $ε$ -neighbourhood of a point of $R$ , Interior, closure, boundary and exterior of a subset of $R$ , Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length).

[L4]

Restriction of the domain (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): if $B \subseteq A$ , if $p \in B$ is a limit point of $B$ and if $h : A \to R$ is differentiable at $p$ , then $h ∣_{B}$ is differentiable at $p$ with $(h ∣_{B})^{'} (p) = h^{'} (p)$ . Moreover every point of an order-convex subset of $R$ with at least two elements is a limit point of it (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, Limit point, isolated point, adherent point, derived set, and dense subset of $R$ ).

[L5]

Continuity passes to a subset of the domain: if $B \subseteq A$ and $h : A \to R$ is continuous at $p \in B$ , then $h ∣_{B}$ is continuous at $p$ (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).

[L6]

Algebra (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, and 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): sums and scalar multiples of functions continuous at a point are continuous there, and sums and scalar multiples of functions differentiable at a limit point of the common domain are differentiable there, with the corresponding derivatives.

Proof

technique · direct

1.1

If $I$ has at most one element then $f$ is constant on $I$ and there is nothing to prove, the second claim following likewise. So assume $I$ has at least two elements and let $u, v \in I$ with $u < v$ be arbitrary.

givenL2

2.1

By [L2] the segment $[u, v]$ is contained in $I$ , and $u < v$ , so $[u, v]$ is a nondegenerate interval. The restriction $f ∣_{[u, v]}$ is continuous on $[u, v]$ by [L5].

step 1.1L2L5

2.2

Let $x \in (u, v)$ . By [L3] the point $x$ is interior to $I$ , so $f$ is differentiable at $x$ with $f^{'} (x) = 0$ by hypothesis. By [L4] the point $x$ is a limit point of $[u, v]$ , so $f ∣_{[u, v]}$ is differentiable at $x$ with $(f ∣_{[u, v]})^{'} (x) = f^{'} (x) = 0$ .

step 1.1L3L4

3.1

By steps 2.1 and 2.2 the function $f ∣_{[u, v]}$ satisfies the hypotheses of [L1] on $[u, v]$ , so there is $c \in (u, v)$ with $f (v) - f (u) = (f ∣_{[u, v]})^{'} (c) (v - u) = 0 \cdot (v - u) = 0$ . Hence $f (u) = f (v)$ .

step 2.1step 2.2L1

4.1

Any two distinct points of $I$ can be named $u$ and $v$ with $u < v$ , and step 3.1 then gives $f (u) = f (v)$ ; at a single point the equality is trivial. So $f$ takes one and the same value at every point of $I$ , and $f$ is constant on $I$ .

step 1.1step 3.1

5.1

Second claim. Put $h : = f + (- 1) g$ , so $h (x) = f (x) - g (x)$ on $I$ . By [L6] the function $h$ is continuous on $I$ . If $I$ has at most one element the claim is trivial; otherwise every point of $I$ is a limit point of $I$ by [L4], so at every interior point $x$ of $I$ the sum rule of [L6] applies and gives that $h$ is differentiable at $x$ with $h^{'} (x) = f^{'} (x) - g^{'} (x) = 0$ . By step 4.1, applied to $h$ in place of $f$ , the function $h$ is constant on $I$ ; writing $k$ for its value, $f (x) = g (x) + k$ for every $x \in I$ .

step 4.1L4L6∎

Remarks

What is really being used. Only that any two points of $I$ are joined by a segment inside $I$ , and that on such a segment the mean value theorem turns a vanishing derivative into a vanishing increment. Both facts are about $I$ , not about $f$ , which is why order-convexity is the hypothesis and not, say, openness or connectedness in some other sense.
The second claim is the uniqueness half of antidifferentiation. It says that a function on an interval is determined by its derivative up to one additive constant. It says nothing about existence: that some given function is a derivative is a separate question, settled by different machinery, and this page does not address it.
A vanishing derivative at every interior point is far stronger than a vanishing derivative somewhere. The theorem consumes the hypothesis at every point of a segment at once; a single stationary point carries no information about $f$ anywhere else, which is what Fermat's interior extremum theorem: if $f$ has a local extremum at a point $c$ interior to its domain and is differentiable at $c$ , then $f^{'} (c) = 0$ already made clear from the other side.

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passverified 2026-08-09 (gpt-5.6-terra-codex-subscription)Open item page →

On an interval $I$ , for $f$ continuous on $I$ and differentiable at every interior point: $f^{'} \geq 0$ throughout gives $f$ nondecreasing, $f^{'} > 0$ gives $f$ increasing, $f^{'} \leq 0$ and $f^{'} < 0$ give the two decreasing forms; conversely a nondecreasing $f$ has $f^{'} \geq 0$ and a nonincreasing $f$ has $f^{'} \leq 0$ wherever it is differentiable, and no strict converse is claimed

Statement

Let $I \subseteq R$ be order-convex (Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length), let $f : I \to R$ be continuous on $I$ (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) and differentiable at every point of $I$ interior to $I$ (Interior, closure, boundary and exterior of a subset of $R$ , 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). The words nondecreasing, increasing, nonincreasing and decreasing are those of Nondecreasing, increasing (strictly increasing), nonincreasing, decreasing, monotone and strictly monotone real functions on a subset of $R$ , with the dictionary to monotone sequences, in which increasing is the strict notion.

If $f^{'} (x) \geq 0$ at every interior point $x$ of $I$ , then $f$ is nondecreasing on $I$ .
If $f^{'} (x) > 0$ at every interior point $x$ of $I$ , then $f$ is increasing on $I$ .
If $f^{'} (x) \leq 0$ at every interior point $x$ of $I$ , then $f$ is nonincreasing on $I$ .
If $f^{'} (x) < 0$ at every interior point $x$ of $I$ , then $f$ is decreasing on $I$ .

Conversely, with no continuity hypothesis and no hypothesis at any other point:

If $f : I \to R$ is nondecreasing on $I$ and differentiable at a point $c \in I$ that is a limit point of $I$ , then $f^{'} (c) \geq 0$ ; if $f$ is nonincreasing and differentiable at such a $c$ , then $f^{'} (c) \leq 0$ .

No strict converse is claimed here, and none is true. Claim 5 gives the weak inequality only, and it cannot be improved: an increasing function may have a vanishing derivative at a point. That failure is recorded separately, as a false statement later on this page, with its witness worked out on the companion page. Reading claim 2 backwards is the single most common misuse of this theorem, and this statement does not license it.

Claims 1 to 4 need the interval; claim 5 does not. The forward direction runs through the mean value theorem on a segment joining two points of $I$ , so order-convexity is essential. Claim 5 is a statement about one point and uses only that the difference quotients have a constant sign.

Facts & Assumptions

Given: An order-convex $I \subseteq R$ and a function $f : I \to R$ ; for claims 1 to 4 also that $f$ is continuous on $I$ and differentiable at every interior point of $I$ , with the stated sign condition; for claim 5 that $f$ is monotone on $I$ and differentiable at a limit point $c \in I$ of $I$ .

[L1]

[L2]

Order-convexity (Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length): $u, v \in I$ with $u \leq v$ gives $[u, v] \subseteq I$ ; and for $u < v$ in $I$ every $x \in (u, v)$ is interior to $I$ , since $N_{ε} (x) \subseteq (u, v) \subseteq I$ for $ε : = \min {x - u, v - x} > 0$ (The $ε$ -neighbourhood and the punctured $ε$ -neighbourhood of a point of $R$ , Interior, closure, boundary and exterior of a subset of $R$ ).

[L3]

Difference quotient and restriction of the domain (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): differentiability of $h$ at $p$ means that $q (x) : = (h (x) - h (p)) / (x - p)$ on $A ∖ {p}$ has limit $h^{'} (p)$ ; if $B \subseteq A$ , if $p \in B$ is a limit point of $B$ and if $h : A \to R$ is differentiable at $p$ , then $h ∣_{B}$ is differentiable at $p$ with the same derivative; and every point of an order-convex set with at least two elements is a limit point of it (Limit point, isolated point, adherent point, derived set, and dense subset of $R$ ).

[L4]

Continuity passes to a subset of the domain (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).

[L5]

Monotone vocabulary (Nondecreasing, increasing (strictly increasing), nonincreasing, decreasing, monotone and strictly monotone real functions on a subset of $R$ , with the dictionary to monotone sequences): $f$ is nondecreasing on $I$ when $f (x) \leq f (y)$ for all $x, y \in I$ with $x \leq y$ ; increasing when $f (x) < f (y)$ for all $x < y$ ; nonincreasing and decreasing are the two conditions with the inequalities on the values reversed.

[L6]

Order arithmetic (Sign rules for products and monotonicity of multiplication, Inverses of positives are positive, and reciprocation reverses order, Ordered field): for reals $s$ and $t$ with $t > 0$ , $s > 0$ gives $s t > 0$ , $s < 0$ gives $s t < 0$ and $s = 0$ gives $s t = 0$ , so by trichotomy $s \geq 0$ gives $s t \geq 0$ and $s \leq 0$ gives $s t \leq 0$ ; a nonzero real and its inverse have the same sign, so a quotient $s / t$ with $s \geq 0$ and $t > 0$ , or with $s \leq 0$ and $t < 0$ , is $\geq 0$ , and a quotient with $s \leq 0$ and $t > 0$ , or with $s \geq 0$ and $t < 0$ , is $\leq 0$ .

[L7]

Limits preserve the non-strict order (If $f \leq g$ on a punctured neighbourhood of $c$ then $\lim f \leq \lim g$ , non-strictly): if $h_{1}, h_{2}$ are functions on a set $D$ having $c$ as a limit point, if both limits at $c$ exist and if $h_{1} \leq h_{2}$ at every $x \in D$ with $0 < ∣ x - c ∣ < η$ for some real $η > 0$ , then $\lim_{x \to c} h_{1} (x) \leq \lim_{x \to c} h_{2} (x)$ . The constant function $0$ on $D$ has limit $0$ at $c$ (The $ε$ - $δ$ limit $\lim_{x \to c} f (x) = L$ of $f : A \to R$ at a limit point $c$ of $A$ ).

Proof

technique · direct

1.1

If $I$ has at most one element then all four of the conditions in [L5] hold on $I$ vacuously or trivially, since there is no pair $x < y$ in $I$ , and claims 1 to 4 are immediate. So assume $I$ has at least two elements, and let $u, v \in I$ with $u < v$ be arbitrary.

givenL5

1.2

Claim 5. Let $f$ be nondecreasing on $I$ and differentiable at a limit point $c \in I$ of $I$ , and let $q (x) : = (f (x) - f (c)) / (x - c)$ on $I ∖ {c}$ , so $\lim_{x \to c} q (x) = f^{'} (c)$ by [L3]. For $x \in I$ with $x > c$ one has $f (x) \geq f (c)$ by [L5], so the numerator is $\geq 0$ while the denominator $x - c$ is $> 0$ , and [L6] gives $q (x) \geq 0$ . For $x \in I$ with $x < c$ one has $f (x) \leq f (c)$ , so the numerator is $\leq 0$ while $x - c < 0$ , and [L6] again gives $q (x) \geq 0$ . So the constant function $0$ is $\leq q$ at every point of $I ∖ {c}$ , in particular at every such point with $0 < ∣ x - c ∣ < 1$ ; both functions have limits at the limit point $c$ of $I ∖ {c}$ , namely $0$ and $f^{'} (c)$ , so [L7] gives $0 \leq f^{'} (c)$ . The nonincreasing case is the same argument with both inequalities on the values reversed, which makes $q \leq 0$ throughout and hence $f^{'} (c) \leq 0$ .

L3L5L6L7

2.1

By [L2] the segment $[u, v]$ is contained in $I$ and is nondegenerate. The restriction $f ∣_{[u, v]}$ is continuous on $[u, v]$ by [L4]; and for $x \in (u, v)$ the point $x$ is interior to $I$ by [L2], so $f$ is differentiable at $x$ , while $x$ is a limit point of $[u, v]$ by [L3], so $f ∣_{[u, v]}$ is differentiable at $x$ with $(f ∣_{[u, v]})^{'} (x) = f^{'} (x)$ .

step 1.1L2L3L4

3.1

By step 2.1 the function $f ∣_{[u, v]}$ satisfies the hypotheses of [L1] on $[u, v]$ , so fix $c \in (u, v)$ with $f (v) - f (u) = f^{'} (c) (v - u)$ ; and $v - u > 0$ since $u < v$ .

step 2.1L1choose

4.1

If $f^{'} (x) \geq 0$ at every interior point of $I$ then in particular $f^{'} (c) \geq 0$ , so $f (v) - f (u) = f^{'} (c) (v - u) \geq 0$ by [L6], that is $f (u) \leq f (v)$ . If $f^{'} (x) > 0$ at every interior point then $f^{'} (c) > 0$ and the same product is $> 0$ , that is $f (u) < f (v)$ .

step 3.1L6

4.2

If $f^{'} (x) \leq 0$ at every interior point then $f^{'} (c) \leq 0$ and $f (v) - f (u) \leq 0$ by [L6], that is $f (u) \geq f (v)$ . If $f^{'} (x) < 0$ at every interior point then $f^{'} (c) < 0$ and $f (v) - f (u) < 0$ , that is $f (u) > f (v)$ .

step 3.1L6

5.1

The pair $u < v$ in $I$ was arbitrary, so steps 4.1 and 4.2 establish exactly the four conditions of [L5]: for the two non-strict ones the case $u = v$ is the trivial equality $f (u) = f (u)$ , and the two strict ones are conditions on pairs $u < v$ only. Claims 1 to 4 are proved.

step 1.1step 4.1step 4.2L5

6.1

Claims 1 to 4 are step 5.1 and claim 5 is step 1.2.

step 1.2step 5.1∎

Remarks

The forward direction is one application of the mean value theorem, and nothing more. The sign of $f^{'}$ at the single point the theorem produces is what decides the sign of the increment; no information about $f^{'}$ anywhere else is used in a given comparison, and the hypothesis is imposed at every interior point only because the point produced cannot be located in advance.
Claim 5 is genuinely weaker than the converse of claim 2, and that is not a defect of the proof. If $f \leq g$ on a punctured neighbourhood of $c$ then $\lim f \leq \lim g$ , non-strictly destroys strictness in the limit, and no argument can restore it here, because the conclusion is false: an increasing function may have a vanishing derivative. The false statement recording that, and its witness on the companion page, are the honest form of what a reader is tempted to write.
What a vanishing derivative at every interior point gives is the case $f^{'} \geq 0$ and $f^{'} \leq 0$ together, hence nondecreasing and nonincreasing, hence constant. That is A function continuous on an interval $I$ whose derivative vanishes at every interior point of $I$ is constant on $I$ ; consequently two such functions with the same derivative differ by a constant, proved directly above rather than deduced here, since the direct proof is shorter.

CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-28Open item page →

If $f$ is continuous on an interval $I$ and $∣ f^{'} ∣ \leq M$ at every interior point, then $∣ f (x) - f (y) ∣ \leq M ∣ x - y ∣$ for all $x, y \in I$ , so $f$ is Lipschitz with constant $M$ and uniformly continuous on $I$

Statement

$∣ f^{'} (x) ∣ \leq M at every interior point x of I .$

Then

$∣ f (x) - f (y) ∣ \leq M ∣ x - y ∣ for all x, y \in I,$

which is exactly the statement that $f$ is Lipschitz with constant $M$ on $I$ (Lipschitz map, $α$ -Hölder map for rational $0 < α \leq 1$ , and contraction, clause 3 of Dictionary: for $A \subseteq R$ with the metric $d (x, y) = ∣ x - y ∣$ , continuity and uniform continuity of $f : A \to R$ agree with the metric-space notions, the Lipschitz and Hölder conditions are the metric ones instantiated, and a subset of $R$ is compact in the open-cover sense of $R$ exactly when it is a compact metric subspace). Consequently $f$ is uniformly continuous on $I$ (Uniform continuity of $f : A \to R$ : one $δ$ serving every pair of points of $A$ ).

$M \geq 0$ is a hypothesis, not a deduction. It follows from $∣ f^{'} (x) ∣ \leq M$ at any single interior point, absolute values being nonnegative, but $I$ need have no interior point at all, and then the sign condition has to be asked for. With $M \geq 0$ assumed the conclusion is a genuine statement in every case, and at $x = y$ it reads $0 \leq 0$ .

Boundedness of $f^{'}$ cannot be dropped. A function may be continuous on an interval and differentiable at every interior point with no bound on $∣ f^{'} ∣$ , and then it need not be Lipschitz there; the companion page's square root on $(0, 1]$ is such a function.

Facts & Assumptions

Given: An order-convex $I \subseteq R$ , a function $f : I \to R$ continuous on $I$ and differentiable at every interior point of $I$ , and a real $M \geq 0$ with $∣ f^{'} (x) ∣ \leq M$ at every interior point $x$ of $I$ .

[L1]

[L2]

[L3]

Restriction of the domain (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): if $B \subseteq A$ , if $p \in B$ is a limit point of $B$ and if $h : A \to R$ is differentiable at $p$ , then $h ∣_{B}$ is differentiable at $p$ with the same derivative; every point of an order-convex set with at least two elements is a limit point of it (Limit point, isolated point, adherent point, derived set, and dense subset of $R$ ).

[L4]

[L5]

Absolute value (Basic properties of the absolute value): $∣ u ∣ \geq 0$ ; $∣ u ∣ = 0$ exactly when $u = 0$ ; $∣ u w ∣ = ∣ u ∣ ∣ w ∣$ ; and $∣ - u ∣ = ∣ u ∣$ , so $∣ x - y ∣ = ∣ y - x ∣$ .

[L6]

Dictionary (Dictionary: for $A \subseteq R$ with the metric $d (x, y) = ∣ x - y ∣$ , continuity and uniform continuity of $f : A \to R$ agree with the metric-space notions, the Lipschitz and Hölder conditions are the metric ones instantiated, and a subset of $R$ is compact in the open-cover sense of $R$ exactly when it is a compact metric subspace, clause 3): for a real $L \geq 0$ , " $f : A \to R$ is Lipschitz with constant $L$ " means exactly that $∣ f (x) - f (x^{'}) ∣ \leq L ∣ x - x^{'} ∣$ for all $x, x^{'} \in A$ , this being the metric condition of Lipschitz map, $α$ -Hölder map for rational $0 < α \leq 1$ , and contraction instantiated at $A \subseteq R$ with $d (x, y) = ∣ x - y ∣$ .

[L7]

Regularity hierarchy (Contraction implies Lipschitz implies uniformly continuous implies continuous; every Hölder map is uniformly continuous, and a Lipschitz map on a bounded space is Hölder for every exponent, claim 2), transported to real functions by clauses 2 and 6 of Dictionary: for $A \subseteq R$ with the metric $d (x, y) = ∣ x - y ∣$ , continuity and uniform continuity of $f : A \to R$ agree with the metric-space notions, the Lipschitz and Hölder conditions are the metric ones instantiated, and a subset of $R$ is compact in the open-cover sense of $R$ exactly when it is a compact metric subspace: a Lipschitz $f : A \to R$ is uniformly continuous on $A$ in the sense of Uniform continuity of $f : A \to R$ : one $δ$ serving every pair of points of $A$ .

[L8]

Multiplying non-strict inequalities of nonnegatives (Multiplying inequalities of positives): $0 \leq s \leq t$ and $0 \leq w \leq z$ imply $s w \leq t z$ .

Proof

technique · direct

1.1

Let $x, y \in I$ . If $x = y$ then $∣ f (x) - f (y) ∣ = ∣ 0 ∣ = 0$ and $M ∣ x - y ∣ = M \cdot 0 = 0$ , so the asserted inequality holds. Assume therefore $x \neq y$ , and put $u : = \min {x, y}$ and $v : = \max {x, y}$ , so that $u, v \in I$ , $u < v$ , and $∣ x - y ∣ = v - u = ∣ v - u ∣$ by [L5].

givenL5

2.1

By [L2] the segment $[u, v]$ lies in $I$ and is nondegenerate; the restriction $f ∣_{[u, v]}$ is continuous on $[u, v]$ by [L4]; and each $x^{'} \in (u, v)$ is interior to $I$ by [L2], hence a point at which $f$ is differentiable with $∣ f^{'} (x^{'}) ∣ \leq M$ , while $x^{'}$ is a limit point of $[u, v]$ by [L3], so $f ∣_{[u, v]}$ is differentiable at $x^{'}$ with the same derivative.

step 1.1L2L3L4

3.1

By step 2.1 the function $f ∣_{[u, v]}$ satisfies the hypotheses of [L1], so fix $c \in (u, v)$ with $f (v) - f (u) = f^{'} (c) (v - u)$ .

step 2.1L1choose

4.1

Taking absolute values in step 3.1 and using $∣ u w ∣ = ∣ u ∣ ∣ w ∣$ gives $∣ f (v) - f (u) ∣ = ∣ f^{'} (c) ∣ ∣ v - u ∣$ . The point $c$ lies in $(u, v)$ , hence is interior to $I$ by step 2.1, so $0 \leq ∣ f^{'} (c) ∣ \leq M$ ; and $0 \leq ∣ v - u ∣ \leq ∣ v - u ∣$ . So [L8] gives $∣ f^{'} (c) ∣ ∣ v - u ∣ \leq M ∣ v - u ∣$ , whence $∣ f (v) - f (u) ∣ \leq M ∣ v - u ∣$ . Since ${u, v} = {x, y}$ and $∣ f (v) - f (u) ∣ = ∣ f (x) - f (y) ∣$ by [L5], and $∣ v - u ∣ = ∣ x - y ∣$ by step 1.1, this is $∣ f (x) - f (y) ∣ \leq M ∣ x - y ∣$ .

step 2.1step 3.1L5L8

5.1

The pair $x, y \in I$ was arbitrary and the case $x = y$ was settled in step 1.1, so $∣ f (x) - f (y) ∣ \leq M ∣ x - y ∣$ for all $x, y \in I$ . By [L6] that is the statement that $f$ is Lipschitz with constant $M$ on $I$ , and by [L7] such an $f$ is uniformly continuous on $I$ .

step 1.1step 4.1L6L7∎

Remarks

The constant is the bound on the derivative, unchanged. No factor is lost and none is gained: the mean value theorem turns the increment into a single value of $f^{'}$ times the increment of the argument, so whatever bounds $∣ f^{'} ∣$ bounds the Lipschitz ratio. That is why this corollary is so much sharper than the mere uniform continuity that follows from it.
Uniform continuity is obtained through the metric dictionary, not reproved. Dictionary: for $A \subseteq R$ with the metric $d (x, y) = ∣ x - y ∣$ , continuity and uniform continuity of $f : A \to R$ agree with the metric-space notions, the Lipschitz and Hölder conditions are the metric ones instantiated, and a subset of $R$ is compact in the open-cover sense of $R$ exactly when it is a compact metric subspace says that the Lipschitz condition for a real function is the metric one instantiated, and Contraction implies Lipschitz implies uniformly continuous implies continuous; every Hölder map is uniformly continuous, and a Lipschitz map on a bounded space is Hölder for every exponent says that a Lipschitz map is uniformly continuous. Neither statement is restated here in an $R$ -native form, because both already exist in the library and duplicating them would create exactly the seam those items were written to close.
What the converse would say, and why it is not asserted. A Lipschitz function need not be differentiable at any particular point, so no statement about $f^{'}$ follows from a Lipschitz bound alone, and this corollary asserts none.
The boundedness hypothesis is exactly what is needed. $x \mapsto \sqrt{x}$ on $(0, 1]$ is differentiable with unbounded derivative and is not Lipschitz there, so the boundedness hypothesis in the Lipschitz corollary cannot be dropped ↗ on the companion page exhibits a function continuous on $(0, 1]$ and differentiable at every interior point, with $∣ f^{'} ∣$ bounded by no real at all, which is not Lipschitz there. So the hypothesis cannot be replaced by mere differentiability, and it cannot be replaced by a bound holding only near one end of the interval.

RemarkRemark: AI-adaptedProof: Not applicablejudge pass (z-ai/glm-5.2)audited 2026-07-28Open item page →

What is fixed here and what is not: the derivative is taken at a point of the domain that is also a limit point of it, one-sided derivatives and derivatives of order above one are not introduced at this point in the reading order, and $f^{'} (c)$ and $\frac{d f}{d x} (c)$ name the same real number

This page fixes fewer conventions than a reader of a calculus text may expect, and it is worth saying which, so that a later page can rely on them and so that nothing here is read as more than it is.

Where a derivative may be taken. $f^{'} (c)$ is defined only when $c$ belongs to the domain $A$ of $f$ and is a limit point of $A$ (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, Limit point, isolated point, adherent point, derived set, and dense subset of $R$ ). At an isolated point of $A$ the symbol is not defined, and the function is neither differentiable nor non-differentiable there: the question is not posed. This is inherited from The $ε$ - $δ$ limit $\lim_{x \to c} f (x) = L$ of $f : A \to R$ at a limit point $c$ of $A$ , which leaves $\lim_{x \to c}$ undefined at an isolated point for the reason recorded there, namely that the $ε$ - $δ$ condition would be satisfied vacuously by every real at once.

The domain is part of the data. "Differentiable at $c$ " is a statement about the pair $(f, A)$ and the point $c$ , not about $f$ near $c$ in isolation. Shrinking the domain preserves differentiability and the value of the derivative whenever the smaller domain still has $c$ as a limit point (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), but enlarging it need not, and the companion page's witness at a corner shows that it need not. Wherever a statement on this page says "differentiable at every point of $(a, b)$ " for a function on $[a, b]$ , the domain meant is $[a, b]$ .

One-sided derivatives are not introduced at this point in the reading order. No item up to this point in the reading order defines one, and nothing below may be cited as though one had been. The ingredient is available: The left and right limits of $f$ at $c$ , as limits of the restrictions of $f$ to $A \cap (- \infty, c)$ and $A \cap (c, \infty)$ defines the limit of $f$ at $c$ from the right as the limit at $c$ of the restriction of $f$ to $A \cap (c, \infty)$ (Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length), and a right derivative would be that limit applied to the difference quotient. Nothing on this page needs it, so nothing on this page defines it. What does occur, and should not be confused with it, is the derivative at an endpoint of an interval: for $f$ on $[a, b]$ the symbol $f^{'} (a)$ is defined by 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 without any new convention, because the domain supplies points on one side of $a$ only and the difference quotient is a function on $(a, b]$ . So the object other texts call a one-sided derivative appears here as an ordinary derivative on a domain that happens to lie on one side.

Derivatives of order above one are not introduced at this point in the reading order either, and no item up to this point in the reading order defines one. A later page takes them up; nothing on this page anticipates it. Doing so requires more than iterating the definition: $f^{'}$ is a function on the set of points at which $f$ is differentiable, and to differentiate that function at a point one needs the point to be a limit point of that set, which is a hypothesis about $f$ and not a formality. No statement on this page mentions $f^{''}$ , and none should be read as implying anything about it.

Two notations, one object. $f^{'} (c)$ and $\frac{d f}{d x} (c)$ name the same real number. The second is a name, not a quotient: nothing in this library divides $d f$ by $d x$ , no object called $d f$ is introduced, and the letter $x$ in it is a name for the argument of $f$ and not a variable that is being fixed or varied. This page writes $f^{'} (c)$ throughout.

What is deliberately not claimed anywhere on this page. That $f^{'}$ is continuous where it exists; that differentiability alone, with no hypothesis on $f^{'}$ , gives any regularity beyond the continuity of A function differentiable at $c$ is continuous at $c$ — a bound on $f^{'}$ does give more, and that is If $f$ is continuous on an interval $I$ and $∣ f^{'} ∣ \leq M$ at every interior point, then $∣ f (x) - f (y) ∣ \leq M ∣ x - y ∣$ for all $x, y \in I$ , so $f$ is Lipschitz with constant $M$ and uniformly continuous on $I$ ; and that a vanishing derivative marks a local extremum. None of the three is addressed here, and no item on this page may be cited for any of them. What is recorded, as the two false statements of this page, is that the mean value theorem needs continuity on the closed interval and that a vanishing derivative at a point does not prevent a function from being increasing; each carries its own witness.

5 · Examples, counterexamples and false statements

False statementConstruction: AI-adaptedVerification: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-28Open item page →

FALSE: differentiability at every point of $(a, b)$ alone yields a $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$

Statement

False claim: let $a, b \in R$ with $a < b$ and let $f : [a, b] \to R$ be differentiable at every point of $(a, b)$ as a function 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, Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length). Then there is $c \in (a, b)$ with

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

This is The mean value theorem, as the case $g (x) = x$ of Cauchy's: for $f$ continuous on $[a, b]$ with $a < b$ and differentiable on $(a, b)$ there is $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$ with the hypothesis " $f$ is continuous on $[a, b]$ " deleted, everything else left as it stands. It is false.

Why it is tempting. The conclusion mentions $f^{'}$ only at interior points, and the hypothesis of continuity on the closed interval looks like a technical condition guaranteeing nothing the differentiability does not already give. It is not: the values $f (a)$ and $f (b)$ appear on the left-hand side of the conclusion, and nothing in a hypothesis about $(a, b)$ alone connects them to the behaviour of $f$ inside. A single unrelated value at one endpoint breaks the identity outright.

Facts & Assumptions

Given: The interval $[0, 1]$ and the function $f : [0, 1] \to R$ defined by $f (x) : = x$ for $x \in [0, 1)$ and $f (1) : = 0$ (Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length).

[L1]

Derivative (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): for $c \in [0, 1]$ a limit point of $[0, 1]$ , the difference quotient $q (x) : = (f (x) - f (c)) / (x - c)$ is a function on $[0, 1] ∖ {c}$ , and $f$ is differentiable at $c$ with $f^{'} (c) = L$ exactly when for every real $ε > 0$ there is a real $δ > 0$ such that every $x \in [0, 1]$ with $0 < ∣ x - c ∣ < δ$ satisfies $∣ q (x) - L ∣ < ε$ (The $ε$ - $δ$ limit $\lim_{x \to c} f (x) = L$ of $f : A \to R$ at a limit point $c$ of $A$ ).

[L2]

Every point of $[0, 1]$ is a limit point of $[0, 1]$ , that set being order-convex with at least two elements (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, Limit point, isolated point, adherent point, derived set, and dense subset of $R$ ).

[L3]

Absolute value and order (Basic properties of the absolute value): $∣ u ∣ \geq 0$ ; $∣ u ∣ = 0$ exactly when $u = 0$ ; and for $δ > 0$ the condition $∣ y - c ∣ < δ$ is $c - δ < y < c + δ$ .

[L4]

$0 \neq 1$ in $R$ , since $0 < 1$ (The multiplicative identity is positive).

[L5]

Continuity at a point (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): $f$ is continuous at $p \in [0, 1]$ when for every real $ε > 0$ there is a real $δ > 0$ such that every $x \in [0, 1]$ with $∣ x - p ∣ < δ$ satisfies $∣ f (x) - f (p) ∣ < ε$ .

[L6]

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)$ ) carries the same continuity hypothesis on the closed interval as The mean value theorem, as the case $g (x) = x$ of Cauchy's: for $f$ continuous on $[a, b]$ with $a < b$ and differentiable on $(a, b)$ there is $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$ does.

Refutation

technique · direct

1.1

$f$ is a well-defined function on $[0, 1]$ : every $x \in [0, 1]$ either equals $1$ or does not, exclusively, so exactly one of the two clauses applies to it.

given

1.2

$f (0) = 0$ , since $0 \in [0, 1)$ , and $f (1) = 0$ by the second clause. Hence $f (1) - f (0) = 0$ , and also $f (0) = f (1)$ .

given

2.1

The derivative inside. Let $c \in (0, 1)$ and put $δ : = \min {c, 1 - c}$ , a positive real. Every $x \in [0, 1]$ with $0 < ∣ x - c ∣ < δ$ satisfies $x < c + δ \leq c + (1 - c) = 1$ by [L3], so $x \in [0, 1)$ and $f (x) = x$ ; and $c \in [0, 1)$ , so $f (c) = c$ . Therefore $q (x) = (x - c) / (x - c) = 1$ for every such $x$ .

step 1.1L3

2.2

$f$ is not continuous at $1$ . Take $ε : = 1 / 2$ and let a real $δ > 0$ be given. Put $x : = \max {1 - δ / 2, 1 / 2}$ ; then $1 / 2 \leq x < 1$ , so $x \in [0, 1)$ and $f (x) = x$ , while $∣ x - 1 ∣ \leq δ / 2 < δ$ . Yet $∣ f (x) - f (1) ∣ = ∣ x - 0 ∣ = x \geq 1 / 2 = ε$ . So no $δ$ witnesses the condition of [L5] at $p = 1$ for this $ε$ .

step 1.1L3L5

3.1

Let $c \in (0, 1)$ and let a real $ε > 0$ be given. The $δ$ of step 2.1 satisfies: every $x \in [0, 1]$ with $0 < ∣ x - c ∣ < δ$ has $∣ q (x) - 1 ∣ = ∣ 1 - 1 ∣ = 0 < ε$ by [L3]. Since $c$ is a limit point of $[0, 1]$ by [L2], this is exactly the condition of [L1] with $L : = 1$ . So $f$ is differentiable at $c$ with $f^{'} (c) = 1$ .

step 2.1L1L2L3

4.1

The claim fails on this witness. By step 3.1 the function $f$ is differentiable at every point of $(0, 1)$ , so it satisfies the hypothesis of the false claim with $a : = 0$ and $b : = 1$ . For every $c \in (0, 1)$ one has $f^{'} (c) (b - a) = 1 \cdot (1 - 0) = 1$ , while $f (b) - f (a) = f (1) - f (0) = 0$ by step 1.2. By [L4] these are different, so no $c \in (0, 1)$ satisfies the asserted identity, and the claim is false.

step 1.2step 3.1L4

5.1

The same witness refutes the corresponding weakening of Rolle's theorem: by step 1.2 one has $f (0) = f (1)$ , and by step 3.1 one has $f^{'} (c) = 1 \neq 0$ at every $c \in (0, 1)$ , so no interior point carries a vanishing derivative. What is missing in both cases is exactly the hypothesis deleted, continuity on the closed interval, and step 2.2 shows it fails at the single point $1$ .

step 1.2step 2.2step 3.1step 4.1L6∎

Remarks

The witness is as small as it can be. It agrees with the identity except at one endpoint, and it is differentiable at every interior point with the constant derivative $1$ . Nothing about the interior is disturbed; only the value $f (1)$ is moved, and the conclusion of the mean value theorem is a statement about that value.
Where the true proof would break. The mean value theorem, as the case $g (x) = x$ of Cauchy's: for $f$ continuous on $[a, b]$ with $a < b$ and differentiable on $(a, b)$ there is $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$ runs through 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)$ , and Rolle runs through Extreme value theorem: a continuous real function on a nonempty compact subset of $R$ attains a greatest and a least value, which needs $f$ continuous on the compact set $[a, b]$ . With continuity failing at $1$ the supremum of $f$ over $[0, 1]$ is $1$ and is not attained, so the extreme value theorem has nothing to hand back and every later step is unavailable.
Continuity at the endpoints is the only thing deleted. In particular the witness is continuous at every point of $(0, 1)$ , being differentiable there; it is even continuous at $0$ . So the false claim cannot be repaired by asking for continuity on $[a, b)$ , or on $(a, b]$ after reflecting the witness, and it is the closed interval that is needed.

False statementConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-28Open item page →

FALSE: if $f^{'} (c) = 0$ then $f$ is not increasing on any interval containing $c$

Statement

False claim: let $I \subseteq R$ be an interval (Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length), let $f : I \to R$ and let $c \in I$ be a point at which $f$ is differentiable with

$f^{'} (c) = 0$

(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 $f$ is not increasing on $I$ , in the strict sense of Nondecreasing, increasing (strictly increasing), nonincreasing, decreasing, monotone and strictly monotone real functions on a subset of $R$ , with the dictionary to monotone sequences.

Why it is tempting. On an interval $I$ , for $f$ continuous on $I$ and differentiable at every interior point: $f^{'} \geq 0$ throughout gives $f$ nondecreasing, $f^{'} > 0$ gives $f$ increasing, $f^{'} \leq 0$ and $f^{'} < 0$ give the two decreasing forms; conversely a nondecreasing $f$ has $f^{'} \geq 0$ and a nonincreasing $f$ has $f^{'} \leq 0$ wherever it is differentiable, and no strict converse is claimed proves that $f^{'} > 0$ at every interior point gives an increasing function, and one reads the implication backwards: if strict increase comes from a strictly positive derivative, surely a derivative that fails to be strictly positive somewhere must destroy the strict increase there. It does not. Claim 5 of that theorem is the true converse, and it is non-strict: an increasing $f$ has $f^{'} \geq 0$ wherever it is differentiable, and nothing forbids equality at isolated points.

Facts & Assumptions

Given: The interval $I : = R$ , the point $c : = 0$ and the function $f : R \to R$ , $f (x) : = x^{3}$ (Integer powers $a^{m}$ , Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length).

[L1]

Power rule (For a natural $n \geq 1$ the function $x \mapsto x^{n}$ is differentiable everywhere with derivative $ι (n) x^{n - 1}$ ; for $n = 0$ it is the constant $1$ , with derivative $0$ ; for a natural $n \geq 1$ the function $x \mapsto x^{- n}$ is differentiable at every $x \neq 0$ with derivative $- ι (n) x^{- n - 1}$ ; consequently every polynomial function is differentiable at every real, with the derivative computed term by term, claim 2): for a natural $n \geq 1$ the function $x \mapsto x^{n}$ is differentiable at every real $c$ with derivative $ι (n) c^{n - 1}$ .

[L2]

Canonical naturals (The canonical natural $ι (n) = n \cdot 1_{F}$ of a field, Canonical naturals are positive and strictly increasing): $ι (n) > 0$ for every natural $n \geq 1$ , so in particular $ι (3) > 0$ .

[L3]

Powers (Integer powers $a^{m}$ ): $a^{0} = 1$ , $a^{2} = a \cdot a$ , and $0 \cdot a = 0$ , so $0^{2} = 0$ .

[L4]

Order arithmetic (Sign rules for products and monotonicity of multiplication, Ordered field): a product of two positive reals is positive and a product of two negative reals is positive; the order is total and transitive, and trichotomy holds.

[L5]

Monotonicity from the derivative (On an interval $I$ , for $f$ continuous on $I$ and differentiable at every interior point: $f^{'} \geq 0$ throughout gives $f$ nondecreasing, $f^{'} > 0$ gives $f$ increasing, $f^{'} \leq 0$ and $f^{'} < 0$ give the two decreasing forms; conversely a nondecreasing $f$ has $f^{'} \geq 0$ and a nonincreasing $f$ has $f^{'} \leq 0$ wherever it is differentiable, and no strict converse is claimed, claim 2): for $J$ order-convex and $h : J \to R$ continuous on $J$ and differentiable at every interior point of $J$ with $h^{'} > 0$ there, $h$ is increasing on $J$ .

[L6]

Continuity (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 5): $x \mapsto x^{n}$ is continuous at every point of its domain for every natural $n$ ; and continuity passes to a subset of the domain (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).

[L7]

Restriction of the derivative (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): if $B \subseteq A$ , if $p \in B$ is a limit point of $B$ and if $h : A \to R$ is differentiable at $p$ , then $h ∣_{B}$ is differentiable at $p$ with the same derivative; every point of an order-convex set with at least two elements is a limit point of it (Limit point, isolated point, adherent point, derived set, and dense subset of $R$ ); and a point $p$ is interior to a set $S$ exactly when $N_{ε} (p) \subseteq S$ for some real $ε > 0$ (The $ε$ -neighbourhood and the punctured $ε$ -neighbourhood of a point of $R$ , Interior, closure, boundary and exterior of a subset of $R$ ).

[L8]

Increasing on a set $J$ means $h (x) < h (y)$ for all $x, y \in J$ with $x < y$ (Nondecreasing, increasing (strictly increasing), nonincreasing, decreasing, monotone and strictly monotone real functions on a subset of $R$ , with the dictionary to monotone sequences).

[L9]

A positive base has positive natural powers (Monotonicity of $x \mapsto x^{n}$ and of $n \mapsto a^{n}$ , claim 1).

Refutation

technique · direct

1.1

By [L1] with $n : = 3$ , the function $f$ is differentiable at every real $c$ with $f^{'} (c) = ι (3) c^{2}$ . In particular $f^{'} (0) = ι (3) \cdot 0^{2} = ι (3) \cdot 0 = 0$ by [L3].

L1L3

1.2

For every real $c \neq 0$ one has $c^{2} > 0$ : if $c > 0$ this is [L9]; if $c < 0$ then $c^{2} = c \cdot c$ is a product of two negative reals, hence positive by [L3] and [L4]. Therefore $f^{'} (c) = ι (3) c^{2} > 0$ for every $c \neq 0$ , being a product of two positive reals by [L2] and [L4].

L2L3L4L9

1.3

Put $I_{1} : = (- \infty, 0]$ and $I_{2} : = [0, \infty)$ , both order-convex with at least two elements (Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length). Every real $x < 0$ is interior to $I_{1}$ , since $N_{∣ x ∣} (x) \subseteq (- \infty, 0) \subseteq I_{1}$ ; and $0$ is not interior to $I_{1}$ , since every $N_{ε} (0)$ contains $ε / 2 > 0$ , which is not in $I_{1}$ . As every interior point of $I_{1}$ lies in $I_{1}$ and so satisfies $x \leq 0$ , the interior points of $I_{1}$ are exactly the reals $x < 0$ . The same argument gives that the interior points of $I_{2}$ are exactly the reals $x > 0$ .

L4L7

2.1

By [L6] the function $f$ is continuous on $R$ , hence $f ∣_{I_{1}}$ is continuous on $I_{1}$ and $f ∣_{I_{2}}$ is continuous on $I_{2}$ . At every interior point $x$ of $I_{1}$ one has $x < 0$ by step 1.3, so $x$ is a limit point of $I_{1}$ by [L7] and $f ∣_{I_{1}}$ is differentiable at $x$ with derivative $f^{'} (x) = ι (3) x^{2} > 0$ by step 1.2 and [L7]. So [L5] gives that $f ∣_{I_{1}}$ is increasing on $I_{1}$ ; the same argument on $I_{2}$ gives that $f ∣_{I_{2}}$ is increasing on $I_{2}$ .

step 1.2step 1.3L5L6L7

3.1

Let $a, b \in R$ with $a < b$ . If $b \leq 0$ then $a, b \in I_{1}$ and step 2.1 gives $f (a) < f (b)$ . If $a \geq 0$ then $a, b \in I_{2}$ and step 2.1 gives $f (a) < f (b)$ . Otherwise $b > 0$ and $a < 0$ , so $a, 0 \in I_{1}$ with $a < 0$ gives $f (a) < f (0)$ , while $0, b \in I_{2}$ with $0 < b$ gives $f (0) < f (b)$ , and transitivity gives $f (a) < f (b)$ . The three cases are exhaustive, since failing both $b \leq 0$ and $a \geq 0$ means $b > 0$ and $a < 0$ . So $f$ is increasing on $R$ by [L8].

step 2.1L4L8

4.1

The false claim fails on this witness: $R$ is an interval, $f$ is differentiable at $c = 0$ with $f^{'} (0) = 0$ by step 1.1, and yet $f$ is increasing on $R$ by step 3.1. So a vanishing derivative forbids nothing of the kind, and the claim is false.

step 1.1step 3.1∎

Remarks

What survives. Claim 5 of On an interval $I$ , for $f$ continuous on $I$ and differentiable at every interior point: $f^{'} \geq 0$ throughout gives $f$ nondecreasing, $f^{'} > 0$ gives $f$ increasing, $f^{'} \leq 0$ and $f^{'} < 0$ give the two decreasing forms; conversely a nondecreasing $f$ has $f^{'} \geq 0$ and a nonincreasing $f$ has $f^{'} \leq 0$ wherever it is differentiable, and no strict converse is claimed is the correct converse and is non-strict: an increasing function differentiable at a point of its interval has $f^{'} \geq 0$ there. This witness saturates that inequality at exactly one point, and no more can be said in general.
How large the vanishing set can be is not settled here. The witness has $f^{'} = 0$ at a single point. Nothing on this page says how big the set ${f^{'} = 0}$ may be for an increasing $f$ , and nothing here should be read as suggesting that it must be small.
The same function is the standard witness for a second false reading, that a vanishing derivative marks a local extremum: $f$ has neither a local maximum nor a local minimum at $0$ , precisely because it is increasing. $x \mapsto x^{3}$ is increasing on $R$ although its derivative vanishes at $0$ , which is the witness for the false statement that a vanishing derivative forbids strict increase, and which makes its inverse non-differentiable at $0$ ↗ on the companion page computes the derivative in full and draws the further consequence, through Derivative of an inverse: if $f$ is continuous and injective on a nondegenerate interval $I$ and differentiable at $c \in I$ with $f^{'} (c) \neq 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)$ , that the inverse of this function is not differentiable at $0$ .

The Derivative and the Mean Value Theorems

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

The derivative f′(c)=lim⁡x→cf(x)−f(c)x−cf′(c)=limx→c​x−cf(x)−f(c)​ of f:A→Rf:A→R at a point c∈Ac∈A that is a limit point of AA, and differentiability on a set

Definition

Remarks

Carathéodory's characterisation: ff is differentiable at cc if and only if there is φ:A→Rφ:A→R, continuous at cc, with f(x)−f(c)=φ(x)(x−c)f(x)−f(c)=φ(x)(x−c) for every x∈Ax∈A, and then φφ is unique and φ(c)=f′(c)φ(c)=f′(c)

Statement

Facts & Assumptions

Proof

Remarks

A function differentiable at cc is continuous at cc

Statement

Facts & Assumptions

Proof

Remarks

Statement

Facts & Assumptions

Proof

Remarks

Statement

Facts & Assumptions

Proof

Remarks

Statement

Facts & Assumptions

Proof

Remarks

The chain rule, in one line from Carathéodory: if gg is differentiable at cc and ff is differentiable at g(c)g(c), then f∘gf∘g is differentiable at cc with (f∘g)′(c)=f′(g(c)) g′(c)(f∘g)′(c)=f′(g(c))g′(c)

Statement

Facts & Assumptions

Proof

Remarks

Statement

Facts & Assumptions

Proof

Remarks

Local (relative) maximum and minimum of f:A→Rf:A→R at a point, the strict forms, and what it means for the point to be interior to AA

Definition

Remarks

Fermat's interior extremum theorem: if ff has a local extremum at a point cc interior to its domain and is differentiable at cc, then f′(c)=0f′(c)=0

Statement

Facts & Assumptions

Proof

Remarks

Rolle's theorem: if a<ba<b, ff is continuous on [a,b][a,b], differentiable at every point of (a,b)(a,b), and f(a)=f(b)f(a)=f(b), then f′(c)=0f′(c)=0 for some c∈(a,b)c∈(a,b)

Statement

Facts & Assumptions

Proof

Remarks

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

Statement

Facts & Assumptions

Proof

Remarks

The mean value theorem, as the case g(x)=xg(x)=x of Cauchy's: for ff 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)=f′(c)(b−a)f(b)−f(a)=f′(c)(b−a)

Statement

Facts & Assumptions

Proof

Remarks

A function continuous on an interval II whose derivative vanishes at every interior point of II is constant on II; consequently two such functions with the same derivative differ by a constant

Statement

Facts & Assumptions

Proof

Remarks

Statement

Facts & Assumptions

Proof

Remarks

If ff is continuous on an interval II and ∣f′∣≤M∣f′∣≤M at every interior point, then ∣f(x)−f(y)∣≤M∣x−y∣∣f(x)−f(y)∣≤M∣x−y∣ for all x,y∈Ix,y∈I, so ff is Lipschitz with constant MM and uniformly continuous on II

Statement

Facts & Assumptions

Proof

Remarks

What is fixed here and what is not: the derivative is taken at a point of the domain that is also a limit point of it, one-sided derivatives and derivatives of order above one are not introduced at this point in the reading order, and f′(c)f′(c) and dfdx(c)dxdf​(c) name the same real number

5 · Examples, counterexamples and false statements

FALSE: differentiability at every point of (a,b)(a,b) alone yields a c∈(a,b)c∈(a,b) with f(b)−f(a)=f′(c)(b−a)f(b)−f(a)=f′(c)(b−a)

Statement

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

Carathéodory's characterisation: $f$ is differentiable at $c$ if and only if there is $φ : A \to R$ , continuous at $c$ , with $f (x) - f (c) = φ (x) (x - c)$ for every $x \in A$ , and then $φ$ is unique and $φ (c) = f^{'} (c)$

A function differentiable at $c$ is continuous at $c$

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)$

Local (relative) maximum and minimum of $f : A \to R$ at a point, the strict forms, and what it means for the point to be interior to $A$

Fermat's interior extremum theorem: if $f$ has a local extremum at a point $c$ interior to its domain and is differentiable at $c$ , then $f^{'} (c) = 0$

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)$

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

The mean value theorem, as the case $g (x) = x$ of Cauchy's: for $f$ continuous on $[a, b]$ with $a < b$ and differentiable on $(a, b)$ there is $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$

A function continuous on an interval $I$ whose derivative vanishes at every interior point of $I$ is constant on $I$ ; consequently two such functions with the same derivative differ by a constant

If $f$ is continuous on an interval $I$ and $∣ f^{'} ∣ \leq M$ at every interior point, then $∣ f (x) - f (y) ∣ \leq M ∣ x - y ∣$ for all $x, y \in I$ , so $f$ is Lipschitz with constant $M$ and uniformly continuous on $I$

What is fixed here and what is not: the derivative is taken at a point of the domain that is also a limit point of it, one-sided derivatives and derivatives of order above one are not introduced at this point in the reading order, and $f^{'} (c)$ and $\frac{d f}{d x} (c)$ name the same real number

FALSE: differentiability at every point of $(a, b)$ alone yields a $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$

FALSE: if $f^{'} (c) = 0$ then $f$ is not increasing on any interval containing $c$