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.

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.

Depends on

Used by

Dependency tree · two levels

29 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

Fermat's theorem (stationary points) (Wikipedia) (standard reference, not scraped)
W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 5 (Thm 5.8) (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)

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