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

How statement and proof provenance work

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

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

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

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.

Depends on

Used by

Dependency tree · two levels

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

Sources

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

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)