Alphabeta Math
Session-authored (Fable 5 assisted)
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.

10 results · all verified · 9 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: Examples and Counterexamples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

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

Worked derivatives from the algebra of derivatives and the power rule: (3x45x+2)=12x35(3x^{4} - 5x + 2)' = 12x^{3} - 5, and the quotient rule applied to (x2+1)/(x1)(x^{2}+1)/(x-1) on R{1}\mathbb{R} \setminus \{1\}

Example

Numerals below denote canonical naturals of R\mathbb{R}: 33 is ι(3)\iota(3), 1212 is ι(12)\iota(12), and so on (The canonical natural ι(n)=n1F\iota(n) = n \cdot 1_F of a field). Powers are those of Integer powers ama^m.

Claim 1. Let p:RRp : \mathbb{R} \to \mathbb{R} be given by

p(x)  =  ι(3)x4    ι(5)x  +  ι(2).p(x) \;=\; \iota(3)\,x^{4} \;-\; \iota(5)\,x \;+\; \iota(2) .

Then pp is differentiable at every cRc \in \mathbb{R} (The derivative f(c)=limxcf(x)f(c)xcf'(c) = \lim_{x \to c} \frac{f(x) - f(c)}{x - c} of f:ARf : A \to \mathbb{R} at a point cAc \in A that is a limit point of AA, and differentiability on a set) and

p(c)  =  ι(12)c3ι(5).p'(c) \;=\; \iota(12)\,c^{3} - \iota(5) .

Claim 2. Put A0:={xR:x10}=R{1}A_0 := \{\, x \in \mathbb{R} : x - 1 \ne 0 \,\} = \mathbb{R} \setminus \{1\} and let r:A0Rr : A_0 \to \mathbb{R} be given by r(x)=(x2+1)/(x1)r(x) = (x^{2}+1)/(x-1). Then every cA0c \in A_0 is a limit point of A0A_0, rr is differentiable at cc as a function on A0A_0, and

r(c)  =  c2ι(2)c1(c1)2.r'(c) \;=\; \frac{c^{2} - \iota(2)c - 1}{(c-1)^{2}} .

Nothing here is new: both computations are readings of Sums, scalar multiples, products and quotients: (f+g)(c)=f(c)+g(c)(f+g)'(c) = f'(c) + g'(c), (αf)(c)=αf(c)(\alpha f)'(c) = \alpha f'(c), (fg)(c)=f(c)g(c)+f(c)g(c)(fg)'(c) = f'(c)g(c) + f(c)g'(c), and (f/g)(c)=(f(c)g(c)f(c)g(c))/g(c)2(f/g)'(c) = \bigl(f'(c)g(c) - f(c)g'(c)\bigr)/g(c)^{2} when g(c)0g(c) \ne 0 on top of For a natural n1n \ge 1 the function xxnx \mapsto x^{n} is differentiable everywhere with derivative ι(n)xn1\iota(n)\,x^{\,n-1}; for n=0n = 0 it is the constant 11, with derivative 00; for a natural n1n \ge 1 the function xxnx \mapsto x^{-n} is differentiable at every x0x \ne 0 with derivative ι(n)xn1-\iota(n)\,x^{-n-1}; consequently every polynomial function is differentiable at every real, with the derivative computed term by term. They are written out because the two places a computation of this kind goes wrong are the constant term, whose derivative is 00 and not ι(0)c1\iota(0)c^{-1}, and the domain of the quotient, which is not R\mathbb{R}.

Facts & Assumptions

Given: The functions pp and rr of the statement, and an arbitrary real cc; for claim 2 also c1c \ne 1.

[L2]

Algebra of derivatives (Sums, scalar multiples, products and quotients: (f+g)(c)=f(c)+g(c)(f+g)'(c) = f'(c) + g'(c), (αf)(c)=αf(c)(\alpha f)'(c) = \alpha f'(c), (fg)(c)=f(c)g(c)+f(c)g(c)(fg)'(c) = f'(c)g(c) + f(c)g'(c), and (f/g)(c)=(f(c)g(c)f(c)g(c))/g(c)2(f/g)'(c) = \bigl(f'(c)g(c) - f(c)g'(c)\bigr)/g(c)^{2} when g(c)0g(c) \ne 0): at a limit point cc of the common domain, sums, scalar multiples and products of functions differentiable at cc are differentiable at cc with the stated formulas; and if the denominator vv is nonzero at cc then, on D0:={x:v(x)0}D_0 := \{x : v(x) \ne 0\}, the point cc lies in D0D_0 and is a limit point of D0D_0, and (u/v)D0(u/v)|_{D_0} is differentiable at cc with derivative (u(c)v(c)u(c)v(c))/v(c)2\bigl(u'(c)v(c) - u(c)v'(c)\bigr)/v(c)^{2}.

[L3]

Canonical naturals (The canonical natural ι(n)=n1F\iota(n) = n \cdot 1_F of a field, Canonical naturals are positive and strictly increasing): ι(1)=1\iota(1) = 1, ι(m+n)=ι(m)+ι(n)\iota(m+n) = \iota(m)+\iota(n) and ι(mn)=ι(m)ι(n)\iota(mn) = \iota(m)\iota(n) for naturals m,n1m, n \ge 1; in particular ι(3)ι(4)=ι(12)\iota(3)\iota(4) = \iota(12) and ι(2)1=1\iota(2) - 1 = 1, the latter from ι(2)=ι(1)+1=1+1\iota(2) = \iota(1) + 1 = 1 + 1.

[L4]

Powers (Integer powers ama^m): x0=1x^{0} = 1, x1=xx^{1} = x and x2=xxx^{2} = x \cdot x.

Verification

technique · direct
1.1

Let cRc \in \mathbb{R}, a limit point of R\mathbb{R} by [L5]. By [L1] the functions xx4x \mapsto x^{4}, xx1x \mapsto x^{1} and xx0x \mapsto x^{0} are differentiable at cc with derivatives ι(4)c3\iota(4)c^{3}, ι(1)c0=1\iota(1)c^{0} = 1 and 00 respectively, using [L4].

L1L4L5
1.2

Put u(x):=x2+1u(x) := x^{2} + 1 and v(x):=x1v(x) := x - 1, both functions on R\mathbb{R}, and let cRc \in \mathbb{R} with c1c \ne 1.

construct
2.1

Claim 1. The function pp is the sum of the scalar multiples ι(3)(xx4)\iota(3)\cdot(x \mapsto x^{4}), (ι(5))(xx1)(-\iota(5))\cdot(x \mapsto x^{1}) and ι(2)(xx0)\iota(2)\cdot(x \mapsto x^{0}), so by the sum and scalar-multiple rules of [L2] it is differentiable at cc with p(c)=ι(3)ι(4)c3+(ι(5))1+ι(2)0=ι(12)c3ι(5)p'(c) = \iota(3)\iota(4)c^{3} + (-\iota(5)) \cdot 1 + \iota(2) \cdot 0 = \iota(12)c^{3} - \iota(5), the last step by [L3].

step 1.1L2L3
2.2

The functions uu and vv are differentiable at every real cc with u(c)=ι(2)cu'(c) = \iota(2)c and v(c)=1v'(c) = 1: uu is the sum of xx2x \mapsto x^{2} and the constant 11, whose derivatives at cc are ι(2)c1=ι(2)c\iota(2)c^{1} = \iota(2)c and 00 by [L1] and [L4]; and vv is the sum of xx1x \mapsto x^{1} and the constant 1-1.

step 1.1L1L2L4
3.1

Claim 2. By step 1.2 one has v(c)=c10v(c) = c - 1 \ne 0, and {xR:v(x)0}\{x \in \mathbb{R} : v(x) \ne 0\} is exactly A0A_0. So the quotient rule of [L2] applies: cA0c \in A_0, the point cc is a limit point of A0A_0, and r=(u/v)A0r = (u/v)|_{A_0} is differentiable at cc with r(c)=(u(c)v(c)u(c)v(c))/v(c)2=(ι(2)c(c1)(c2+1))/(c1)2r'(c) = \bigl(u'(c)v(c) - u(c)v'(c)\bigr)/v(c)^{2} = \bigl(\iota(2)c\,(c-1) - (c^{2}+1)\bigr)/(c-1)^{2}.

step 1.2step 2.2L2
4.1

Expanding the numerator: ι(2)c(c1)(c2+1)=ι(2)c2ι(2)cc21=(ι(2)1)c2ι(2)c1=c2ι(2)c1\iota(2)c(c-1) - (c^{2}+1) = \iota(2)c^{2} - \iota(2)c - c^{2} - 1 = \bigl(\iota(2)-1\bigr)c^{2} - \iota(2)c - 1 = c^{2} - \iota(2)c - 1, the last equality because ι(2)1=1\iota(2) - 1 = 1 by [L3]. So r(c)=(c2ι(2)c1)/(c1)2r'(c) = \bigl(c^{2} - \iota(2)c - 1\bigr)/(c-1)^{2}.

step 3.1L3L4
5.1

Both claims are verified: claim 1 by step 2.1 and claim 2 by steps 3.1 and 4.1.

step 2.1step 4.1

Remarks

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

xxx \mapsto |x| is continuous everywhere and not differentiable at 00: the difference quotient equals 11 on the right and 1-1 on the left, so the two one-sided limits differ

Statement refuted

Refuted claim: if ARA \subseteq \mathbb{R}, if f:ARf : A \to \mathbb{R} is continuous at a point cAc \in A (Continuity of f:ARf : A \to \mathbb{R} at a point of AA and on AA: the ε\varepsilon-δ\delta condition, its agreement with limxcf(x)=f(c)\lim_{x \to c} f(x) = f(c) at a limit point, and continuity at an isolated point) and if cc is a limit point of AA (Limit point, isolated point, adherent point, derived set, and dense subset of R\mathbb{R}), then ff is differentiable at cc (The derivative f(c)=limxcf(x)f(c)xcf'(c) = \lim_{x \to c} \frac{f(x) - f(c)}{x - c} of f:ARf : A \to \mathbb{R} at a point cAc \in A that is a limit point of AA, and differentiability on a set).

This is the converse of A function differentiable at cc is continuous at cc, and it is false. The witness is f(x)=xf(x) = |x| on A=RA = \mathbb{R} at c=0c = 0: a single corner is enough, and the failure is visible in one line, the difference quotient taking the value 11 to the right of 00 and 1-1 to the left.

Facts & Assumptions

Given: The set A:=RA := \mathbb{R}, the function f:RRf : \mathbb{R} \to \mathbb{R}, f(x):=xf(x) := |x| (Basic properties of the absolute value), and the point c:=0c := 0.

[L3]

Absolute value (Basic properties of the absolute value): 0=0|0| = 0; u=u|u| = u for u0u \ge 0; and u=u|u| = -u for u0u \le 0.

[L4]

One-sided limits (The left and right limits of ff at cc, as limits of the restrictions of ff to A(,c)A \cap (-\infty, c) and A(c,)A \cap (c, \infty), Intervals of R\mathbb{R}: the nine order-convex forms, nondegeneracy, and length): for DRD \subseteq \mathbb{R} and pRp \in \mathbb{R}, the right limit of h:DRh : D \to \mathbb{R} at pp is the limit at pp of hh restricted to D(p,)D \cap (p, \infty), defined when pp is a limit point of that set, and the left limit is the same with D(,p)D \cap (-\infty, p).

[L5]

Two-sided against one-sided (If cc is a limit point of the domain from both sides, the limit exists iff both one-sided limits exist and agree): if pp is a limit point of both D(,p)D \cap (-\infty,p) and D(p,)D \cap (p,\infty), then for every real LL the equality limxph(x)=L\lim_{x \to p} h(x) = L holds if and only if both one-sided limits at pp exist and equal LL.

[L6]

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); and the limit of a constant function KK at a limit point of its domain is KK, any δ\delta serving (The ε\varepsilon-δ\delta limit limxcf(x)=L\lim_{x \to c} f(x) = L of f:ARf : A \to \mathbb{R} at a limit point cc of AA).

[L7]

111 \ne -1: 0<10 < 1 (The multiplicative identity is positive) gives 1<0<1-1 < 0 < 1, and trichotomy forbids equality.

Counterexample

technique · direct
1.1

ff is continuous at every point of R\mathbb{R}, in particular at 00.

L1
1.2

f(0)=0=0f(0) = |0| = 0, so the difference quotient of ff at 00 is q(x)=x/xq(x) = |x|/x on D:=R{0}D := \mathbb{R} \setminus \{0\}.

L2L3
1.3

D(0,)=(0,)D \cap (0,\infty) = (0,\infty) and D(,0)=(,0)D \cap (-\infty,0) = (-\infty,0), and 00 is a limit point of each: for every real ε>0\varepsilon > 0 the point ε/2\varepsilon/2 lies in (0,)(0,\infty) with 0<ε/20<ε0 < |\varepsilon/2 - 0| < \varepsilon, and ε/2-\varepsilon/2 lies in (,0)(-\infty,0) with 0<ε/20<ε0 < |-\varepsilon/2 - 0| < \varepsilon.

L3L4
2.1

For x>0x > 0 one has x=x|x| = x, so q(x)=x/x=1q(x) = x/x = 1; for x<0x < 0 one has x=x|x| = -x, so q(x)=(x)/x=1q(x) = (-x)/x = -1. Thus qq restricted to (0,)(0,\infty) is the constant 11 and qq restricted to (,0)(-\infty,0) is the constant 1-1.

step 1.2L3
3.1

By [L6] and step 1.3 the two restrictions have limits at 00, namely 11 and 1-1; so by [L4] the right limit of qq at 00 is 11 and the left limit is 1-1.

step 1.3step 2.1L4L6
4.1

Suppose limx0q(x)=L\lim_{x \to 0} q(x) = L for some real LL. By step 1.3 the point 00 is a limit point of both one-sided sets, so [L5] forces both one-sided limits to equal LL; with step 3.1 and [L6] that gives L=1L = 1 and L=1L = -1, hence 1=11 = -1, which [L7] forbids. So qq has no limit at 00, and by [L2] the function ff is not differentiable at 00.

step 3.1L2L5L6L7
5.1

The refuted claim therefore fails at A:=RA := \mathbb{R}, f:=f := |\cdot| and c:=0c := 0: the point 00 is a limit point of R\mathbb{R}, ff is continuous at 00 by step 1.1, and ff is not differentiable at 00 by step 4.1.

step 1.1step 4.1

Remarks

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

xx3x \mapsto x^{3} is increasing on R\mathbb{R} although its derivative vanishes at 00, which is the witness for the false statement that a vanishing derivative forbids strict increase, and which makes its inverse non-differentiable at 00

Example

Let f:RRf : \mathbb{R} \to \mathbb{R} be f(x)=x3f(x) = x^{3} (Integer powers ama^m), with ι\iota the canonical natural of The canonical natural ι(n)=n1F\iota(n) = n \cdot 1_F of a field.

Claim 1. ff is differentiable at every cRc \in \mathbb{R} with f(c)=ι(3)c2f'(c) = \iota(3)c^{2}, and f(0)=0f'(0) = 0.

Claim 2. ff is increasing on R\mathbb{R}, in the strict sense of Nondecreasing, increasing (strictly increasing), nonincreasing, decreasing, monotone and strictly monotone real functions on a subset of R\mathbb{R}, with the dictionary to monotone sequences.

Claim 3. So the hypothesis "f>0f' > 0 at every interior point" of claim 2 of On an interval II, for ff continuous on II and differentiable at every interior point: f0f' \ge 0 throughout gives ff nondecreasing, f>0f' > 0 gives ff increasing, f0f' \le 0 and f<0f' < 0 give the two decreasing forms; conversely a nondecreasing ff has f0f' \ge 0 and a nonincreasing ff has f0f' \le 0 wherever it is differentiable, and no strict converse is claimed is sufficient but not necessary for a function on an interval to be increasing; and the converse recorded there, claim 5, which gives only f0f' \ge 0, cannot be strengthened to f>0f' > 0.

Claim 4. ff is continuous and injective on R\mathbb{R}, so it has a continuous inverse gg on f[R]f[\mathbb{R}] (Derivative of an inverse: if ff is continuous and injective on a nondegenerate interval II and differentiable at cIc \in I with f(c)0f'(c) \ne 0, then the inverse gg is differentiable at f(c)f(c) with g(f(c))=1/f(c)g'(f(c)) = 1/f'(c); and if f(c)=0f'(c) = 0 then gg is not differentiable at f(c)f(c)); and since f(0)=0f'(0) = 0, that inverse is not differentiable at f(0)=0f(0) = 0.

Claims 1 and 2 are established in the refutation of FALSE: if f(c)=0f'(c) = 0 then ff is not increasing on any interval containing cc and are quoted here; claims 3 and 4 are the two consequences worth drawing from them.

Facts & Assumptions

Given: The function f:RRf : \mathbb{R} \to \mathbb{R}, f(x)=x3f(x) = x^{3}.

[L5]

Derivative of an inverse (Derivative of an inverse: if ff is continuous and injective on a nondegenerate interval II and differentiable at cIc \in I with f(c)0f'(c) \ne 0, then the inverse gg is differentiable at f(c)f(c) with g(f(c))=1/f(c)g'(f(c)) = 1/f'(c); and if f(c)=0f'(c) = 0 then gg is not differentiable at f(c)f(c)): for II order-convex with at least two elements and f:IRf : I \to \mathbb{R} continuous and injective, with inverse g:f[I]Ig : f[I] \to I, and for cIc \in I at which ff is differentiable, if f(c)=0f'(c) = 0 then gg is not differentiable at f(c)f(c).

[L7]

03=00^{3} = 0, since 0n=00^{n} = 0 for every natural n1n \ge 1 (Integer powers ama^m).

Verification

technique · direct
1.1

Claims 1 and 2. By [L1] the function ff is differentiable at every cRc \in \mathbb{R} with f(c)=ι(3)c2f'(c) = \iota(3)c^{2}, its derivative at 00 is 00, and ff is increasing on R\mathbb{R}.

L1
2.1

ff is injective by [L2], being increasing; it is continuous on R\mathbb{R} by [L3]; and R\mathbb{R} is order-convex with at least two elements by [L4]. So ff satisfies every hypothesis of [L5] with I:=RI := \mathbb{R}.

step 1.1L2L3L4L5
2.2

Claim 3. The hypothesis of claim 2 of [L6] fails for ff on R\mathbb{R}, since f(0)=0f'(0) = 0 is not positive, and yet the conclusion holds, ff being increasing on R\mathbb{R} by step 1.1. So that hypothesis is sufficient and not necessary. Likewise the conclusion f0f' \ge 0 of claim 5 of [L6] is attained with equality at 00 by step 1.1, so it cannot be strengthened to f>0f' > 0.

step 1.1L6
3.1

Claim 4. By step 2.1 the hypotheses of [L5] hold, and by step 1.1 the function ff is differentiable at 00 with f(0)=0f'(0) = 0. So [L5] gives that the inverse g:f[R]Rg : f[\mathbb{R}] \to \mathbb{R} is not differentiable at f(0)f(0), which is 00 by [L7].

step 1.1step 2.1L5L7
4.1

All four claims are verified: claims 1 and 2 by step 1.1, claim 3 by step 2.2 and claim 4 by step 3.1.

step 1.1step 2.2step 3.1

Remarks

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

The chain rule applied to x(x2+1)5x \mapsto (x^{2}+1)^{5} and to x((3x1)2+2)3x \mapsto ((3x-1)^{2}+2)^{3}, with the Carathéodory factor written out in closed form in the first case

Example

Numerals denote canonical naturals of R\mathbb{R} (The canonical natural ι(n)=n1F\iota(n) = n \cdot 1_F of a field) and powers are those of Integer powers ama^m.

Claim 1. Let F:RRF : \mathbb{R} \to \mathbb{R} be F(x)=(x2+1)5F(x) = (x^{2}+1)^{5}. Then FF is differentiable at every cRc \in \mathbb{R} (The derivative f(c)=limxcf(x)f(c)xcf'(c) = \lim_{x \to c} \frac{f(x) - f(c)}{x - c} of f:ARf : A \to \mathbb{R} at a point cAc \in A that is a limit point of AA, and differentiability on a set) and

F(c)  =  ι(10)c(c2+1)4.F'(c) \;=\; \iota(10)\,c\,(c^{2}+1)^{4} .

Claim 2. For bRb \in \mathbb{R} the Carathéodory factor (Carathéodory's characterisation: ff is differentiable at cc if and only if there is φ:AR\varphi : A \to \mathbb{R}, continuous at cc, with f(x)f(c)=φ(x)(xc)f(x) - f(c) = \varphi(x)(x - c) for every xAx \in A, and then φ\varphi is unique and φ(c)=f(c)\varphi(c) = f'(c)) of yy5y \mapsto y^{5} at bb is the polynomial function

φ(y)  =  k<5bky4k,\varphi(y) \;=\; \sum_{k<5} b^{k}\,y^{\,4-k} ,

which satisfies y5b5=φ(y)(yb)y^{5} - b^{5} = \varphi(y)(y-b) for every yRy \in \mathbb{R}, is continuous at bb, and has φ(b)=ι(5)b4\varphi(b) = \iota(5)b^{4}.

Claim 3. Let G:RRG : \mathbb{R} \to \mathbb{R} be G(x)=((ι(3)x1)2+2)3G(x) = \bigl((\iota(3)x-1)^{2}+2\bigr)^{3}. Then GG is differentiable at every cRc \in \mathbb{R} and

G(c)  =  ι(18)(ι(3)c1)((ι(3)c1)2+2)2.G'(c) \;=\; \iota(18)\,(\iota(3)c-1)\,\bigl((\iota(3)c-1)^{2}+2\bigr)^{2} .

Claim 2 is included because it makes the mechanism of the chain rule visible: the factor that the proof of 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 fgf \circ g is differentiable at cc with (fg)(c)=f(g(c))g(c)(f \circ g)'(c) = f'(g(c))\,g'(c) takes from Carathéodory's characterisation: ff is differentiable at cc if and only if there is φ:AR\varphi : A \to \mathbb{R}, continuous at cc, with f(x)f(c)=φ(x)(xc)f(x) - f(c) = \varphi(x)(x - c) for every xAx \in A, and then φ\varphi is unique and φ(c)=f(c)\varphi(c) = f'(c) is, for a power, an explicit polynomial, and no auxiliary case distinction is hidden inside it.

Facts & Assumptions

Given: The functions FF, φ\varphi and GG of the statement, and an arbitrary real cc.

[L1]

Chain rule (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 fgf \circ g is differentiable at cc with (fg)(c)=f(g(c))g(c)(f \circ g)'(c) = f'(g(c))\,g'(c)): with g:ARg : A \to \mathbb{R}, g[A]Bg[A] \subseteq B, f:BRf : B \to \mathbb{R}, cAc \in A a limit point of AA at which gg is differentiable, and b:=g(c)Bb := g(c) \in B a limit point of BB at which ff is differentiable, the composite fgf \circ g is differentiable at cc with (fg)(c)=f(g(c))g(c)(f \circ g)'(c) = f'(g(c))g'(c).

[L4]

Carathéodory's characterisation (Carathéodory's characterisation: ff is differentiable at cc if and only if there is φ:AR\varphi : A \to \mathbb{R}, continuous at cc, with f(x)f(c)=φ(x)(xc)f(x) - f(c) = \varphi(x)(x - c) for every xAx \in A, and then φ\varphi is unique and φ(c)=f(c)\varphi(c) = f'(c)): ff is differentiable at a limit point pp of its domain if and only if some η\eta continuous at pp satisfies f(y)f(p)=η(y)(yp)f(y)-f(p) = \eta(y)(y-p) throughout, and then η(p)=f(p)\eta(p) = f'(p); the factor is unique.

[L5]

Factorisation of a difference of powers (Factorisation of bnanb^n - a^n, and the resulting Lipschitz estimate): for reals s,ts, t and a natural n1n \ge 1, tnsn=(ts)k<nsktn1kt^{n} - s^{n} = (t-s)\sum_{k<n} s^{k} t^{\,n-1-k} (Finite sums and finite products, by recursion).

[L6]

Finite sums (Laws of finite sums and finite products, claim 2): k<nλ=ι(n)λ\sum_{k<n} \lambda = \iota(n)\lambda for a constant λ\lambda; and powers combine as bkbn1k=bn1b^{k}b^{\,n-1-k} = b^{\,n-1} for kn1k \le n-1 (Laws of integer exponents).

[L8]

Canonical naturals (The canonical natural ι(n)=n1F\iota(n) = n \cdot 1_F of a field, Canonical naturals are positive and strictly increasing): ι(mn)=ι(m)ι(n)\iota(mn) = \iota(m)\iota(n) for naturals m,n1m, n \ge 1, so ι(5)ι(2)=ι(10)\iota(5)\iota(2) = \iota(10), ι(2)ι(3)=ι(6)\iota(2)\iota(3) = \iota(6) and ι(3)ι(6)=ι(18)\iota(3)\iota(6) = \iota(18); and ι(1)=1\iota(1) = 1.

Verification

technique · direct
1.1

Put g(x):=x2+1g(x) := x^{2} + 1 and f(y):=y5f(y) := y^{5}, both on R\mathbb{R}. By [L2] and [L3] the function gg is differentiable at every real cc with g(c)=ι(2)cg'(c) = \iota(2)c, and ff is differentiable at every real bb with f(b)=ι(5)b4f'(b) = \iota(5)b^{4}.

L2L3
1.2

Put u(x):=ι(3)x1u(x) := \iota(3)x - 1, v(y):=y2+2v(y) := y^{2} + 2 and w(z):=z3w(z) := z^{3}, all on R\mathbb{R}. By [L2] and [L3], u(c)=ι(3)u'(c) = \iota(3), v(b)=ι(2)bv'(b) = \iota(2)b and w(a)=ι(3)a2w'(a) = \iota(3)a^{2} at every real argument.

L2L3
2.1

Claim 2. Fix bRb \in \mathbb{R} and put φ(y):=k<5bky4k\varphi(y) := \sum_{k<5} b^{k}y^{\,4-k} for yRy \in \mathbb{R}. Applying [L5] with n:=5n := 5, s:=bs := b and t:=yt := y gives y5b5=(yb)k<5bky4k=φ(y)(yb)y^{5} - b^{5} = (y - b)\sum_{k<5} b^{k} y^{\,4-k} = \varphi(y)(y-b) for every real yy. As a finite sum of scalar multiples of powers of yy, the function φ\varphi is a polynomial function and so is continuous at bb by [L7]. Finally φ(b)=k<5bkb4k=k<5b4=ι(5)b4\varphi(b) = \sum_{k<5} b^{k}b^{\,4-k} = \sum_{k<5} b^{4} = \iota(5)b^{4} by [L6]. So φ\varphi is the factor of [L4] for ff at bb, and [L4] returns f(b)=φ(b)=ι(5)b4f'(b) = \varphi(b) = \iota(5)b^{4}, in agreement with step 1.1.

L4L5L6L7
2.2

Claim 1. By [L9] every real is a limit point of R\mathbb{R}, and gg maps R\mathbb{R} into R\mathbb{R}, so [L1] applies to F=fgF = f \circ g at any cc: FF is differentiable at cc with F(c)=f(g(c))g(c)=ι(5)(c2+1)4ι(2)c=ι(10)c(c2+1)4F'(c) = f'(g(c))\,g'(c) = \iota(5)(c^{2}+1)^{4}\cdot \iota(2)c = \iota(10)\,c\,(c^{2}+1)^{4}, the last step by [L8].

step 1.1L1L8L9
2.3

Claim 3. By [L1] and [L9], applied first to vuv \circ u and then to w(vu)w \circ (v \circ u), the function G=w(vu)G = w \circ (v \circ u) is differentiable at every real cc, with (vu)(c)=v(u(c))u(c)=ι(2)(ι(3)c1)ι(3)=ι(6)(ι(3)c1)(v \circ u)'(c) = v'(u(c))u'(c) = \iota(2)(\iota(3)c-1)\cdot\iota(3) = \iota(6)(\iota(3)c-1) and then G(c)=w((vu)(c))(vu)(c)=ι(3)((ι(3)c1)2+2)2ι(6)(ι(3)c1)=ι(18)(ι(3)c1)((ι(3)c1)2+2)2G'(c) = w'\bigl((v \circ u)(c)\bigr)\,(v \circ u)'(c) = \iota(3)\bigl((\iota(3)c-1)^{2}+2\bigr)^{2}\cdot\iota(6)(\iota(3)c-1) = \iota(18)(\iota(3)c-1)\bigl((\iota(3)c-1)^{2}+2\bigr)^{2}, the collapsing of the numerals by [L8].

step 1.2L1L8L9
3.1

The three claims are verified: claim 1 by step 2.2, claim 2 by step 2.1 and claim 3 by step 2.3.

step 2.1step 2.2step 2.3

Remarks

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

For a natural n1n \ge 1, the derivative of xx1/nx \mapsto x^{1/n} on (0,)(0,\infty) is 1ι(n)x1/n1\frac{1}{\iota(n)}x^{1/n - 1}, obtained from the inverse rule applied to xxnx \mapsto x^{n}; in particular (x)=1/(ι(2)x)(\sqrt{x})' = 1/(\iota(2)\sqrt{x})

Example

Let nNn \in \mathbb{N} with n1n \ge 1, let ι\iota be the canonical natural of The canonical natural ι(n)=n1F\iota(n) = n \cdot 1_F of a field, and let rational powers be those of Rational powers ara^r of a positive base, so that u1/nu^{1/n} is the unique nonnegative nn-th root of uu (Existence and uniqueness of nn-th roots: a unique a1/n0a^{1/n} \ge 0 with (a1/n)n=a(a^{1/n})^n = a).

Claim. The function

g:(0,)R,g(u):=u1/n,g : (0,\infty) \to \mathbb{R}, \qquad g(u) := u^{1/n},

is differentiable at every b(0,)b \in (0,\infty) (The derivative f(c)=limxcf(x)f(c)xcf'(c) = \lim_{x \to c} \frac{f(x) - f(c)}{x - c} of f:ARf : A \to \mathbb{R} at a point cAc \in A that is a limit point of AA, and differentiability on a set), and

g(b)  =  1ι(n)  b1/n1.g'(b) \;=\; \frac{1}{\iota(n)}\; b^{\,1/n - 1} .

In particular at n=2n = 2, writing u=u1/2\sqrt{u} = u^{1/2},

g(b)  =  1ι(2)b1/2  =  1ι(2)b.g'(b) \;=\; \frac{1}{\iota(2)}\,b^{-1/2} \;=\; \frac{1}{\iota(2)\sqrt{b}} .

The domain is (0,)(0,\infty) and not [0,)[0,\infty), and the reason depends on nn. For n2n \ge 2 the exponent 1/n11/n - 1 is a negative rational, and Rational powers ara^r of a positive base leaves 0r0^{r} undefined for rational r<0r < 0, so at b=0b = 0 the displayed formula is not a statement at all; and the root really is not differentiable there, by claim 2 of Derivative of an inverse: if ff is continuous and injective on a nondegenerate interval II and differentiable at cIc \in I with f(c)0f'(c) \ne 0, then the inverse gg is differentiable at f(c)f(c) with g(f(c))=1/f(c)g'(f(c)) = 1/f'(c); and if f(c)=0f'(c) = 0 then gg is not differentiable at f(c)f(c) applied on [0,)[0,\infty), since xxnx \mapsto x^{n} has derivative ι(n)0n1=0\iota(n)\,0^{\,n-1} = 0 at 00 for n2n \ge 2 (For a natural n1n \ge 1 the function xxnx \mapsto x^{n} is differentiable everywhere with derivative ι(n)xn1\iota(n)\,x^{\,n-1}; for n=0n = 0 it is the constant 11, with derivative 00; for a natural n1n \ge 1 the function xxnx \mapsto x^{-n} is differentiable at every x0x \ne 0 with derivative ι(n)xn1-\iota(n)\,x^{-n-1}; consequently every polynomial function is differentiable at every real, with the derivative computed term by term, Integer powers ama^m). At n=1n = 1 neither obstruction arises: the exponent 1/n11/n - 1 is 00, not negative; u1/1=uu^{1/1} = u is the identity (Existence and uniqueness of nn-th roots: a unique a1/n0a^{1/n} \ge 0 with (a1/n)n=a(a^{1/n})^n = a); and the formula reads g(b)=b0=1g'(b) = b^{0} = 1, which is correct at every real. So for n=1n = 1 the restriction to (0,)(0,\infty) is a convenience of the uniform statement rather than a necessity. Nothing below asserts anything about the root at 00 in either case.

Facts & Assumptions

Given: A natural n1n \ge 1, the set I:=(0,)I := (0,\infty), the function f:IRf : I \to \mathbb{R}, f(x):=xnf(x) := x^{n}, and the function g:IRg : I \to \mathbb{R}, g(u):=u1/ng(u) := u^{1/n}.

[L1]

Roots (Existence and uniqueness of nn-th roots: a unique a1/n0a^{1/n} \ge 0 with (a1/n)n=a(a^{1/n})^n = a): for every real a0a \ge 0 and every natural n1n \ge 1 there is a unique real s0s \ge 0 with sn=as^{n} = a, written a1/na^{1/n}; and a1/n>0a^{1/n} > 0 when a>0a > 0. By Rational powers ara^r of a positive base the rational power a1/na^{1/n} is that same number.

[L2]

Rational power laws (Laws of rational exponents): for a>0a > 0 and rationals r,sr, s one has ar>0a^{r} > 0, (ar)s=ars(a^{r})^{s} = a^{rs}, ar+s=arasa^{r+s} = a^{r}a^{s} and ar=1/ara^{-r} = 1/a^{r}; and rational powers extend integer powers on positive bases (Rational powers ara^r of a positive base, Integer powers ama^m).

[L3]

Monotonicity of integer powers (Monotonicity of xxnx \mapsto x^n and of nann \mapsto a^n): for a natural n1n \ge 1 the map xxnx \mapsto x^{n} is strictly increasing on {x0}\{x \ge 0\}, hence injective there (claim 2); and x>0x > 0 implies xn>0x^{n} > 0 (claim 1).

[L6]

Derivative of an inverse (Derivative of an inverse: if ff is continuous and injective on a nondegenerate interval II and differentiable at cIc \in I with f(c)0f'(c) \ne 0, then the inverse gg is differentiable at f(c)f(c) with g(f(c))=1/f(c)g'(f(c)) = 1/f'(c); and if f(c)=0f'(c) = 0 then gg is not differentiable at f(c)f(c), claim 1): for II order-convex with at least two elements and f:IRf : I \to \mathbb{R} continuous and injective with inverse g:f[I]Ig : f[I] \to I, if ff is differentiable at cIc \in I with f(c)0f'(c) \ne 0 then gg is differentiable at f(c)f(c) with g(f(c))=1/f(c)g'(f(c)) = 1/f'(c).

[L7]

Verification

technique · direct
1.1

I=(0,)I = (0,\infty) is order-convex with at least two elements, and every point of II is a limit point of II.

L8
1.2

ff is injective on II by [L3], continuous on II by [L4], and takes only positive values by [L3].

L3L4
1.3

f[I]=If[I] = I. For xIx \in I one has f(x)=xn>0f(x) = x^{n} > 0 by [L3], so f[I]If[I] \subseteq I; and for uIu \in I the number u1/nu^{1/n} is positive by [L1], hence lies in II, and f(u1/n)=(u1/n)n=uf(u^{1/n}) = (u^{1/n})^{n} = u by [L1], so uf[I]u \in f[I].

L1L3
2.1

The map g:IIg : I \to I, uu1/nu \mapsto u^{1/n}, is the inverse of f:If[I]=If : I \to f[I] = I. By [L7] and step 1.2 that bijection has a unique two-sided inverse; by step 1.3 the map gg takes values in II and satisfies f(g(u))=uf(g(u)) = u for every uIu \in I, so it is a right inverse of the bijection and therefore is that unique inverse.

step 1.2step 1.3L1L7
2.2

ff is differentiable at every cIc \in I with f(c)=ι(n)cn1f'(c) = \iota(n)c^{\,n-1}, by [L5] together with step 1.1; and f(c)0f'(c) \ne 0, since ι(n)>0\iota(n) > 0 by [L8] and cn1>0c^{\,n-1} > 0 by [L3] as c>0c > 0.

step 1.1L3L5L8
3.1

Let bIb \in I and put c:=b1/nc := b^{1/n}, an element of II by [L1], with f(c)=bf(c) = b by [L1]. By step 1.2, step 2.2 and [L6], applied on II at cc, the inverse gg is differentiable at b=f(c)b = f(c) with g(b)=1/f(c)=1/(ι(n)cn1)g'(b) = 1/f'(c) = 1/\bigl(\iota(n)\,c^{\,n-1}\bigr).

step 2.1step 2.2L1L6
4.1

Rewriting in terms of bb: since c=b1/nc = b^{1/n} and n1n - 1 is a natural, [L2] gives cn1=(b1/n)n1=b(n1)/n=b11/nc^{\,n-1} = \bigl(b^{1/n}\bigr)^{\,n-1} = b^{\,(n-1)/n} = b^{\,1 - 1/n}, a positive real. Hence g(b)=1/(ι(n)b11/n)=1ι(n)b(11/n)=1ι(n)b1/n1g'(b) = 1/\bigl(\iota(n)\,b^{\,1-1/n}\bigr) = \frac{1}{\iota(n)}\,b^{-(1-1/n)} = \frac{1}{\iota(n)}\,b^{\,1/n - 1}, using ar=1/ara^{-r} = 1/a^{r} from [L2] and ι(n)0\iota(n) \ne 0 from [L8].

step 3.1L2L8
5.1

At n=2n = 2 the map gg is uu1/2=uu \mapsto u^{1/2} = \sqrt{u}, and step 4.1 reads g(b)=1ι(2)b1/21=1ι(2)b1/2=1ι(2)bg'(b) = \frac{1}{\iota(2)}b^{\,1/2 - 1} = \frac{1}{\iota(2)}b^{-1/2} = \frac{1}{\iota(2)\sqrt{b}}, again by [L2].

step 4.1L2

Remarks

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

f(x)=xf(x) = x on [0,1)[0,1) with f(1)=0f(1) = 0 is differentiable at every point of (0,1)(0,1) with f1f' \equiv 1, yet no cc satisfies f(1)f(0)=f(c)f(1) - f(0) = f'(c), so continuity on the closed interval cannot be dropped from the mean value theorem

Statement refuted

Refuted claim: let a,bRa, b \in \mathbb{R} with a<ba < b and let f:[a,b]Rf : [a,b] \to \mathbb{R} be differentiable at every point of (a,b)(a,b) as a function on [a,b][a,b] (The derivative f(c)=limxcf(x)f(c)xcf'(c) = \lim_{x \to c} \frac{f(x) - f(c)}{x - c} of f:ARf : A \to \mathbb{R} at a point cAc \in A that is a limit point of AA, and differentiability on a set). Then there is c(a,b)c \in (a,b) with f(b)f(a)=f(c)(ba)f(b) - f(a) = f'(c)(b-a).

That is 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 \in (a,b) with f(b)f(a)=f(c)(ba)f(b) - f(a) = f'(c)(b-a) with the hypothesis of continuity on [a,b][a,b] deleted, and it is false; the false statement itself is recorded as FALSE: differentiability at every point of (a,b)(a,b) alone yields a c(a,b)c \in (a,b) with f(b)f(a)=f(c)(ba)f(b) - f(a) = f'(c)(b-a). This item works the witness out: it locates the failure at a single point, measures it, and shows that repairing that one value restores the conclusion.

Facts & Assumptions

Given: The function f:[0,1]Rf : [0,1] \to \mathbb{R} with f(x):=xf(x) := x for x[0,1)x \in [0,1) and f(1):=0f(1) := 0, and the identity h:[0,1]Rh : [0,1] \to \mathbb{R}, h(x):=xh(x) := x (Intervals of R\mathbb{R}: the nine order-convex forms, nondegeneracy, and length).

[L1]

The refutation of FALSE: differentiability at every point of (a,b)(a,b) alone yields a c(a,b)c \in (a,b) with f(b)f(a)=f(c)(ba)f(b) - f(a) = f'(c)(b-a) establishes, for this ff: that ff is differentiable at every c(0,1)c \in (0,1) with f(c)=1f'(c) = 1; that f(0)=f(1)=0f(0) = f(1) = 0, so f(1)f(0)=0f(1) - f(0) = 0; and that no c(0,1)c \in (0,1) satisfies f(1)f(0)=f(c)(10)f(1)-f(0) = f'(c)(1-0).

[L2]

One-sided limits (The left and right limits of ff at cc, as limits of the restrictions of ff to A(,c)A \cap (-\infty, c) and A(c,)A \cap (c, \infty), Intervals of R\mathbb{R}: the nine order-convex forms, nondegeneracy, and length): the left limit of ff at pp is the limit at pp of ff restricted to [0,1](,p)[0,1] \cap (-\infty,p), defined when pp is a limit point of that set; the right limit is the same with [0,1](p,)[0,1] \cap (p,\infty).

[L3]

The limit condition (The ε\varepsilon-δ\delta limit limxcf(x)=L\lim_{x \to c} f(x) = L of f:ARf : A \to \mathbb{R} at a limit point cc of AA): limxpu(x)=L\lim_{x \to p} u(x) = L means that for every real ε>0\varepsilon > 0 there is a real δ>0\delta > 0 such that every xx in the domain of uu with 0<xp<δ0 < |x - p| < \delta satisfies u(x)L<ε|u(x) - L| < \varepsilon. The clause 0<xp0 < |x-p| removes x=px = p from the quantifier (Basic properties of the absolute value, The ε\varepsilon-neighbourhood and the punctured ε\varepsilon-neighbourhood of a point of R\mathbb{R}).

[L4]

Continuity at a limit point (Continuity of f:ARf : A \to \mathbb{R} at a point of AA and on AA: the ε\varepsilon-δ\delta condition, its agreement with limxcf(x)=f(c)\lim_{x \to c} f(x) = f(c) at a limit point, and continuity at an isolated point, clause 1): for p[0,1]p \in [0,1] a limit point of [0,1][0,1], the function ff is continuous at pp if and only if limxpf(x)\lim_{x \to p} f(x) exists and equals f(p)f(p).

[L7]

010 \ne 1, since 0<10 < 1 (The multiplicative identity is positive).

Counterexample

technique · direct
1.1

By [L1] the function ff is differentiable at every c(0,1)c \in (0,1) with f(c)=1f'(c) = 1, satisfies f(0)=f(1)=0f(0) = f(1) = 0, and admits no c(0,1)c \in (0,1) with f(1)f(0)=f(c)(10)f(1)-f(0) = f'(c)(1-0). So the refuted claim fails at a:=0a := 0, b:=1b := 1.

L1
1.2

The point 11 is a limit point of [0,1][0,1] and of [0,1](,1)=[0,1)[0,1] \cap (-\infty,1) = [0,1): for every real ε>0\varepsilon > 0 the point y:=max{1ε/2, 1/2}y := \max\{1-\varepsilon/2,\ 1/2\} satisfies 1/2y<11/2 \le y < 1, hence y[0,1)y \in [0,1), and 0<y1ε/2<ε0 < |y - 1| \le \varepsilon/2 < \varepsilon.

L2L3
2.1

limx1f(x)=1\lim_{x \to 1} f(x) = 1, the limit taken over the domain [0,1][0,1]. Given a real ε>0\varepsilon > 0, take δ:=ε\delta := \varepsilon; every x[0,1]x \in [0,1] with 0<x1<δ0 < |x - 1| < \delta has x1x \ne 1 by [L3], hence x[0,1)x \in [0,1) and f(x)=xf(x) = x, so f(x)1=x1<ε|f(x) - 1| = |x-1| < \varepsilon. Since the same quantifier ranges over the same points when the domain is cut down to [0,1)[0,1), this also says limx1f(x)=1\lim_{x \to 1^{-}} f(x) = 1 by [L2]. The right limit at 11 is not defined, since [0,1](1,)[0,1] \cap (1,\infty) is empty and 11 is therefore not a limit point of it.

step 1.2L2L3
3.1

ff is not continuous at 11. By step 1.2 the point 11 is a limit point of [0,1][0,1], so [L4] makes continuity there equivalent to limx1f(x)=f(1)\lim_{x \to 1} f(x) = f(1); by step 2.1 the left side is 11 and by [L1] the right side is 00, and 010 \ne 1 by [L7]. So exactly one hypothesis of [L5] fails, at exactly one point, and it is the deleted one.

step 2.1L1L4L5L7
4.1

The repair. The identity hh agrees with ff at every point of [0,1][0,1] except 11, where h(1)=1h(1) = 1 and f(1)=0f(1) = 0. By [L6] the function hh is continuous on [0,1][0,1] and differentiable at every point of (0,1)(0,1) with h(c)=1h'(c) = 1, so [L5] applies to hh; and indeed h(1)h(0)=1=1(10)=h(c)(10)h(1) - h(0) = 1 = 1 \cdot (1-0) = h'(c)(1-0) for every c(0,1)c \in (0,1). So moving the single value f(1)f(1) back to 11 turns a function with no admissible cc into one for which every cc is admissible.

step 1.1step 3.1L5L6
5.1

The same witness refutes the corresponding weakening of Rolle's theorem: f(0)=f(1)=0f(0) = f(1) = 0 by step 1.1, and yet f(c)=10f'(c) = 1 \ne 0 at every c(0,1)c \in (0,1) by step 1.1 and [L7]. So neither theorem in [L5] survives the deletion of continuity on the closed interval.

step 1.1step 4.1L5L7

Remarks

  • The discontinuity is of the mildest possible kind. Both of the quantities that exist at 11, the left limit and the value, exist and are finite; they simply differ. In the vocabulary of the page on monotone functions and discontinuities this is a removable discontinuity, and step 4.1 removes it. Nothing pathological is needed to break the mean value theorem.

  • Why the derivative sees nothing. The difference quotient of ff at an interior cc is evaluated only at points within min{c,1c}\min\{c, 1-c\} of cc, and every such point lies in [0,1)[0,1), where ff is the identity. So ff' carries no information at all about f(1)f(1), while the conclusion of the mean value theorem is an equation containing f(1)f(1). Continuity on the closed interval is precisely the bridge between the two.

  • Reflecting the witness covers the other endpoint. The function xf(1x)x \mapsto -f(1-x) is differentiable at every point of (0,1)(0,1) with the same constant derivative and fails continuity at 00 instead of at 11, so nothing is special about which endpoint is broken.

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

The identity on [0,1][0,1] attains its maximum at 11 and its minimum at 00 with derivative 11 at both, so Fermat's theorem genuinely needs the extremum to be at an interior point

Statement refuted

Refuted claim: let ARA \subseteq \mathbb{R}, let f:ARf : A \to \mathbb{R} and let cAc \in A be a limit point of AA at which ff has a local extremum (Local (relative) maximum and minimum of f:ARf : A \to \mathbb{R} at a point, the strict forms, and what it means for the point to be interior to AA) and is differentiable (The derivative f(c)=limxcf(x)f(c)xcf'(c) = \lim_{x \to c} \frac{f(x) - f(c)}{x - c} of f:ARf : A \to \mathbb{R} at a point cAc \in A that is a limit point of AA, and differentiability on a set). Then f(c)=0f'(c) = 0.

That is 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 with the hypothesis "cc is interior to AA" deleted and replaced by the weaker one needed for f(c)f'(c) to be a defined symbol at all. It is false: the identity on [0,1][0,1] attains a greatest and a least value, both at points of the domain that are not interior to it, and its derivative is 11 everywhere.

Facts & Assumptions

Given: The set A:=[0,1]A := [0,1] (Intervals of R\mathbb{R}: the nine order-convex forms, nondegeneracy, and length) and the function f:ARf : A \to \mathbb{R}, f(x):=xf(x) := x.

[L1]

Derivative of the identity (The derivative f(c)=limxcf(x)f(c)xcf'(c) = \lim_{x \to c} \frac{f(x) - f(c)}{x - c} of f:ARf : A \to \mathbb{R} at a point cAc \in A that is a limit point of AA, and differentiability on a set, The ε\varepsilon-δ\delta limit limxcf(x)=L\lim_{x \to c} f(x) = L of f:ARf : A \to \mathbb{R} at a limit point cc of AA): every point of the order-convex set [0,1][0,1], which has at least two elements, is a limit point of it (Limit point, isolated point, adherent point, derived set, and dense subset of R\mathbb{R}); and the difference quotient of ff at any c[0,1]c \in [0,1] is (xc)/(xc)=1(x-c)/(x-c) = 1 at every x[0,1]x \in [0,1] with xcx \ne c, a constant function whose limit at cc is 11. So ff is differentiable at every c[0,1]c \in [0,1] with f(c)=1f'(c) = 1.

[L2]

Local extrema (Local (relative) maximum and minimum of f:ARf : A \to \mathbb{R} at a point, the strict forms, and what it means for the point to be interior to AA): ff has a local maximum at cAc \in A when f(x)f(c)f(x) \le f(c) for every xANε(c)x \in A \cap N_{\varepsilon}(c) for some real ε>0\varepsilon > 0, and a local minimum with the inequality reversed; a value that is a greatest value of ff over the whole of AA is a local maximum, and a least value is a local minimum (claim 4 of its body); and cc is interior to AA exactly when Nε(c)AN_{\varepsilon}(c) \subseteq A for some real ε>0\varepsilon > 0 (Interior, closure, boundary and exterior of a subset of R\mathbb{R}, The ε\varepsilon-neighbourhood and the punctured ε\varepsilon-neighbourhood of a point of R\mathbb{R}).

[L3]

Maximum and minimum of a set (Maximum and minimum of a set): mm is a maximum of SS when mSm \in S and sms \le m for every sSs \in S, and a minimum when mSm \in S and msm \le s for every sSs \in S.

[L5]

010 \ne 1, since 0<10 < 1 (The multiplicative identity is positive).

Counterexample

technique · direct
1.1

By [L1] the function ff is differentiable at every c[0,1]c \in [0,1], and f(c)=1f'(c) = 1; in particular f(0)=f(1)=1f'(0) = f'(1) = 1, and every point of [0,1][0,1] is a limit point of [0,1][0,1].

L1
1.2

Every xAx \in A satisfies 0x10 \le x \le 1, so f(x)=x1=f(1)f(x) = x \le 1 = f(1) and f(x)=x0=f(0)f(x) = x \ge 0 = f(0); and 0,1A0, 1 \in A. So f(1)f(1) is a maximum of f[A]f[A] and f(0)f(0) is a minimum of f[A]f[A] by [L3], and by [L2] the function ff has a local maximum at 11 and a local minimum at 00, hence a local extremum at each.

L2L3
1.3

Neither 11 nor 00 is interior to AA: for every real ε>0\varepsilon > 0 the point 1+ε/21 + \varepsilon/2 lies in Nε(1)N_{\varepsilon}(1) and not in [0,1][0,1], and the point ε/2-\varepsilon/2 lies in Nε(0)N_{\varepsilon}(0) and not in [0,1][0,1]. So no NεN_{\varepsilon} around either point is contained in AA.

L2
2.1

The refuted claim therefore fails at c:=1c := 1: the point 11 lies in AA and is a limit point of AA by step 1.1, ff has a local extremum there by step 1.2 and is differentiable there by step 1.1, and yet f(1)=10f'(1) = 1 \ne 0 by [L5]. The same holds at c:=0c := 0.

step 1.1step 1.2L5
3.1

Nothing in [L4] is contradicted. By step 1.3 neither 00 nor 11 is interior to AA, so the hypothesis of that theorem is not met at either point, and the deleted hypothesis is exactly the one that fails. Indeed no point of AA at all carries a vanishing derivative, and consistently with [L4] no interior point of AA carries a local extremum: by step 1.2 the only extrema of ff over AA sit at the two endpoints.

step 1.3step 2.1L4

Remarks

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

The mean value theorem gives xy1ι(2)xy|\sqrt{x} - \sqrt{y}| \le \tfrac{1}{\iota(2)} |x - y| for x,y1x, y \ge 1, so the square root is Lipschitz with constant 1/21/2 on [1,)[1,\infty)

Example

Write b=b1/2\sqrt{b} = b^{1/2} for the nonnegative square root (Existence and uniqueness of nn-th roots: a unique a1/n0a^{1/n} \ge 0 with (a1/n)n=a(a^{1/n})^n = a, Rational powers ara^r of a positive base) and ι\iota for the canonical natural (The canonical natural ι(n)=n1F\iota(n) = n \cdot 1_F of a field).

Claim. Let I:=[1,)I := [1,\infty) and let s:IRs : I \to \mathbb{R}, s(b):=bs(b) := \sqrt{b}. Then

xy    1ι(2)xyfor all x,yI,|\sqrt{x} - \sqrt{y}| \;\le\; \frac{1}{\iota(2)}\,|x - y| \qquad \text{for all } x, y \in I ,

so ss is Lipschitz with constant 1/ι(2)1/\iota(2) on II (Lipschitz map, α\alpha-Hölder map for rational 0<α10 < \alpha \le 1, and contraction, clause 3 of Dictionary: for ARA \subseteq \mathbb{R} with the metric d(x,y)=xyd(x,y) = |x-y|, continuity and uniform continuity of f:ARf : A \to \mathbb{R} agree with the metric-space notions, the Lipschitz and Hölder conditions are the metric ones instantiated, and a subset of R\mathbb{R} is compact in the open-cover sense of R\mathbb{R} exactly when it is a compact metric subspace) and hence uniformly continuous on II (Uniform continuity of f:ARf : A \to \mathbb{R}: one δ\delta serving every pair of points of AA).

The constant is what the derivative bound gives, and the domain is what makes the bound available. On [1,)[1,\infty) the derivative of ss is at most 1/ι(2)1/\iota(2); on (0,1](0,1] it is not bounded at all, and the companion counterexample on this page shows that there the Lipschitz conclusion fails.

Facts & Assumptions

Given: The set I:=[1,)I := [1,\infty), order-convex with at least two elements (Intervals of R\mathbb{R}: the nine order-convex forms, nondegeneracy, and length), and the function s:IRs : I \to \mathbb{R}, s(b):=b1/2s(b) := b^{1/2}.

[L1]

Derivative of the square root (For a natural n1n \ge 1, the derivative of xx1/nx \mapsto x^{1/n} on (0,)(0,\infty) is 1ι(n)x1/n1\frac{1}{\iota(n)}x^{1/n - 1}, obtained from the inverse rule applied to xxnx \mapsto x^{n}; in particular (x)=1/(ι(2)x)(\sqrt{x})' = 1/(\iota(2)\sqrt{x}), at n=2n = 2): the map uu1/2u \mapsto u^{1/2} on (0,)(0,\infty) is differentiable at every b>0b > 0 with derivative 1ι(2)b1/2\frac{1}{\iota(2)}b^{-1/2}.

[L3]

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

[L4]

Rational powers (Laws of rational exponents, Monotonicity of rarr \mapsto a^{r} and of aara \mapsto a^{r}, Existence and uniqueness of nn-th roots: a unique a1/n0a^{1/n} \ge 0 with (a1/n)n=a(a^{1/n})^n = a): ar>0a^{r} > 0 for a>0a > 0; ar=1/ara^{-r} = 1/a^{r}; 11/2=11^{1/2} = 1, since 101 \ge 0 and 12=11^{2} = 1 and the nonnegative square root is unique; and for rational t>0t > 0, a>1a > 1 implies at>1a^{t} > 1 (claim 3 of the monotonicity lemma).

[L5]

Order arithmetic (Inverses of positives are positive, and reciprocation reverses order, Sign rules for products and monotonicity of multiplication, Canonical naturals are positive and strictly increasing, Multiplying inequalities of positives): ι(2)>0\iota(2) > 0, so 1/ι(2)>01/\iota(2) > 0 and ι(2)0\iota(2) \ne 0; 0<a<b0 < a < b gives 0<1/b<1/a0 < 1/b < 1/a (Inverses of positives are positive, and reciprocation reverses order); a product of two positive reals is positive (Sign rules for products and monotonicity of multiplication); and the NONSTRICT multiplication of inequalities between nonnegatives, 0xy0 \le x \le y and 0uv0 \le u \le v imply xuyvxu \le yv, is Multiplying inequalities of positives and is not stated by Sign rules for products and monotonicity of multiplication, whose multiplicative claims are strict. Also u=u|u| = u for u0u \ge 0 (Basic properties of the absolute value).

[L6]

Interiority (Interior, closure, boundary and exterior of a subset of R\mathbb{R}, The ε\varepsilon-neighbourhood and the punctured ε\varepsilon-neighbourhood of a point of R\mathbb{R}): pp is interior to SS exactly when Nε(p)SN_{\varepsilon}(p) \subseteq S for some real ε>0\varepsilon > 0.

Verification

technique · direct
1.1

The interior points of I=[1,)I = [1,\infty) are exactly the reals b>1b > 1. For b>1b > 1 the neighbourhood Nb1(b)N_{b-1}(b) is contained in (1,)I(1,\infty) \subseteq I, so bb is interior; the point 11 is not interior, since 1ε/2Nε(1)1 - \varepsilon/2 \in N_{\varepsilon}(1) and 1ε/2I1 - \varepsilon/2 \notin I for every real ε>0\varepsilon > 0; and every interior point of II lies in II, hence is 1\ge 1.

L6
1.2

For every real b1b \ge 1 one has b1/21b^{-1/2} \le 1. If b=1b = 1 then 11/2=11^{1/2} = 1 by [L4], so 11/2=1/1=11^{-1/2} = 1/1 = 1. If b>1b > 1 then b1/2>1b^{1/2} > 1 by [L4], and b1/2>0b^{1/2} > 0, so b1/2=1/b1/2<1b^{-1/2} = 1/b^{1/2} < 1 by [L4] and [L5].

L4L5
2.1

By [L1] and [L2] the function ss is differentiable at every bIb \in I with s(b)=1ι(2)b1/2s'(b) = \frac{1}{\iota(2)}b^{-1/2}, and by [L3] it is continuous at every point of II, hence continuous on II.

step 1.1L1L2L3
3.1

At every interior point bb of II one has b>1b > 1 by step 1.1, so b1/2>0b^{-1/2} > 0 by [L4] and b1/21b^{-1/2} \le 1 by step 1.2; multiplying the pair 0b1/210 \le b^{-1/2} \le 1 and 01/ι(2)1/ι(2)0 \le 1/\iota(2) \le 1/\iota(2) as in [L5] gives 0<s(b)1/ι(2)0 < s'(b) \le 1/\iota(2) by step 2.1, and therefore s(b)=s(b)1/ι(2)|s'(b)| = s'(b) \le 1/\iota(2) by [L5].

step 1.1step 1.2step 2.1L4L5
4.1

Apply [L7] with J:=IJ := I, h:=sh := s and M:=1/ι(2)M := 1/\iota(2), a real 0\ge 0 by [L5]: the hypotheses hold by step 2.1 for the continuity and differentiability and by step 3.1 for the bound, so s(x)s(y)1ι(2)xy|s(x)-s(y)| \le \frac{1}{\iota(2)}|x-y| for all x,yIx, y \in I, that is xy1ι(2)xy|\sqrt{x} - \sqrt{y}| \le \frac{1}{\iota(2)}|x-y|; ss is Lipschitz with constant 1/ι(2)1/\iota(2) on II; and ss is uniformly continuous on II.

step 2.1step 3.1L5L7

Remarks

CounterexampleConstruction: AI-adaptedVerification: AI-generatedprecheck passverified 2026-08-09 (gpt-5.6-terra-codex-subscription)Open item page →

xxx \mapsto \sqrt{x} on (0,1](0,1] is differentiable with unbounded derivative and is not Lipschitz there, so the boundedness hypothesis in the Lipschitz corollary cannot be dropped

Statement refuted

Refuted claim: let IRI \subseteq \mathbb{R} be order-convex (Intervals of R\mathbb{R}: the nine order-convex forms, nondegeneracy, and length) and let h:IRh : I \to \mathbb{R} be continuous on II and differentiable at every interior point of II (The derivative f(c)=limxcf(x)f(c)xcf'(c) = \lim_{x \to c} \frac{f(x) - f(c)}{x - c} of f:ARf : A \to \mathbb{R} at a point cAc \in A that is a limit point of AA, and differentiability on a set). Then hh is Lipschitz on II, that is, there is a real L0L \ge 0 with h(x)h(y)Lxy|h(x)-h(y)| \le L|x-y| for all x,yIx, y \in I (Lipschitz map, α\alpha-Hölder map for rational 0<α10 < \alpha \le 1, and contraction, clause 3 of Dictionary: for ARA \subseteq \mathbb{R} with the metric d(x,y)=xyd(x,y) = |x-y|, continuity and uniform continuity of f:ARf : A \to \mathbb{R} agree with the metric-space notions, the Lipschitz and Hölder conditions are the metric ones instantiated, and a subset of R\mathbb{R} is compact in the open-cover sense of R\mathbb{R} exactly when it is a compact metric subspace).

That is If ff is continuous on an interval II and fM|f'| \le M at every interior point, then f(x)f(y)Mxy|f(x) - f(y)| \le M|x-y| for all x,yIx,y \in I, so ff is Lipschitz with constant MM and uniformly continuous on II with the hypothesis hM|h'| \le M deleted. It is false, and the witness is the square root on (0,1](0,1]: an interval on which the derivative exists at every interior point and is bounded above by no real.

Facts & Assumptions

Given: The set I:=(0,1]I := (0,1], order-convex with at least two elements (Intervals of R\mathbb{R}: the nine order-convex forms, nondegeneracy, and length), and the function s:IRs : I \to \mathbb{R}, s(b):=b1/2s(b) := b^{1/2}, the nonnegative square root (Existence and uniqueness of nn-th roots: a unique a1/n0a^{1/n} \ge 0 with (a1/n)n=a(a^{1/n})^n = a, Rational powers ara^r of a positive base); numerals denote canonical naturals (The canonical natural ι(n)=n1F\iota(n) = n \cdot 1_F of a field).

[L2]

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

[L3]

Uniqueness of the nonnegative square root (Existence and uniqueness of nn-th roots: a unique a1/n0a^{1/n} \ge 0 with (a1/n)n=a(a^{1/n})^n = a): for a0a \ge 0 there is exactly one t0t \ge 0 with t2=at^{2} = a, and it is a1/2a^{1/2} (Rational powers ara^r of a positive base, Integer powers ama^m).

[L4]

Rational powers (Laws of rational exponents, Monotonicity of rarr \mapsto a^{r} and of aara \mapsto a^{r}): ar>0a^{r} > 0 for a>0a > 0; ar=1/ara^{-r} = 1/a^{r}; (ar)s=ars(a^{r})^{s} = a^{rs}; and for rational r>0r > 0, 0<a<b0 < a < b implies ar<bra^{r} < b^{r} (claim 2 of the monotonicity lemma).

[L5]

Archimedean property in reciprocal form (For every ε>0\varepsilon > 0 in a complete ordered field there is a natural n1n \ge 1 with 1/n<ε1/n < \varepsilon, Every complete ordered field is Archimedean): for every real ε>0\varepsilon > 0 there is a natural m1m \ge 1 with 1/ι(m)<ε1/\iota(m) < \varepsilon.

[L6]

Order and numeral arithmetic (Inverses of positives are positive, and reciprocation reverses order, Sign rules for products and monotonicity of multiplication, Multiplying inequalities of positives, Canonical naturals are positive and strictly increasing, Monotonicity of xxnx \mapsto x^n and of nann \mapsto a^n, Basic properties of the absolute value, The canonical natural ι(n)=n1F\iota(n) = n \cdot 1_F of a field): ι(m)>0\iota(m) > 0 for m1m \ge 1; 0<a<b0 < a < b gives 0<1/b<1/a0 < 1/b < 1/a (Inverses of positives are positive, and reciprocation reverses order); a product of positives is positive and multiplying a STRICT inequality by a positive real preserves it (Sign rules for products and monotonicity of multiplication); the NONSTRICT form, 0xy0 \le x \le y and 0uv0 \le u \le v imply xuyvxu \le yv, is not stated by Sign rules for products and monotonicity of multiplication, whose multiplicative claims are strict, but by Multiplying inequalities of positives, and it is what licenses both multiplying a \le by a positive real and dividing a \le by one, the divisor entering as its positive inverse; 0ab0 \le a \le b gives a2b2a^{2} \le b^{2} (Monotonicity of xxnx \mapsto x^n and of nann \mapsto a^n, claim 2); u=u|u| = u for u0u \ge 0 (Basic properties of the absolute value); and ι(mn)=ι(m)ι(n)\iota(mn) = \iota(m)\iota(n) and ι(m+n)=ι(m)+ι(n)\iota(m+n) = \iota(m)+\iota(n) for naturals m,n1m, n \ge 1, so ι(2)2=ι(4)\iota(2)^{2} = \iota(4), ι(2)1=1\iota(2) - 1 = 1 and ι(4)1=ι(3)\iota(4) - 1 = \iota(3).

[L7]

Interiority and boundedness (Interior, closure, boundary and exterior of a subset of R\mathbb{R}, The ε\varepsilon-neighbourhood and the punctured ε\varepsilon-neighbourhood of a point of R\mathbb{R}, Lower bound, bounded below, bounded set): pp is interior to SS exactly when Nε(p)SN_{\varepsilon}(p) \subseteq S for some real ε>0\varepsilon > 0; and a set of reals is bounded above when some real exceeds or equals all of its elements.

Counterexample

technique · direct
1.1

By [L1] the function ss is differentiable at every bIb \in I with s(b)=1ι(2)b1/2>0s'(b) = \frac{1}{\iota(2)}b^{-1/2} > 0, using [L4] and [L6]; and by [L2] it is continuous at every point of II, hence continuous on II.

L1L2L4L6
1.2

The interior points of I=(0,1]I = (0,1] are exactly the reals bb with 0<b<10 < b < 1: for such a bb the neighbourhood Nρ(b)N_{\rho}(b) with ρ:=min{b, 1b}>0\rho := \min\{b,\ 1-b\} > 0 lies in (0,1)I(0,1) \subseteq I; the point 11 is not interior, since 1+ε/2Nε(1)1 + \varepsilon/2 \in N_{\varepsilon}(1) and 1+ε/2I1 + \varepsilon/2 \notin I for every real ε>0\varepsilon > 0; and every interior point lies in II.

L7
2.1

The derivative is bounded above by no real. Let KK be a real. If K0K \le 0, any bb with 0<b<10 < b < 1 has s(b)>0Ks'(b) > 0 \ge K by step 1.1. If K>0K > 0, put β:=(1/(ι(2)K))2\beta := \bigl(1/(\iota(2)K)\bigr)^{2}, a positive real, and use [L5] to fix a natural m1m \ge 1 with 1/ι(m)<min{β, 1}1/\iota(m) < \min\{\beta,\ 1\}; put b:=1/ι(m)b := 1/\iota(m), so 0<b<10 < b < 1 and b<βb < \beta. By [L4], b1/2<β1/2=(1/(ι(2)K))2(1/2)=1/(ι(2)K)b^{1/2} < \beta^{1/2} = \bigl(1/(\iota(2)K)\bigr)^{2 \cdot (1/2)} = 1/(\iota(2)K), so b1/2=1/b1/2>ι(2)Kb^{-1/2} = 1/b^{1/2} > \iota(2)K by [L6], and hence s(b)=1ι(2)b1/2>Ks'(b) = \frac{1}{\iota(2)}b^{-1/2} > K. So for every real KK there is an interior point bb of II with s(b)>Ks'(b) > K, and the set of values of ss' on the interior of II is bounded above by no real.

step 1.1step 1.2L4L5L6L7
2.2

ss is not Lipschitz on II. Suppose some real L0L \ge 0 satisfied s(x)s(y)Lxy|s(x)-s(y)| \le L|x-y| for all x,yIx, y \in I. Let tt be a real with 0<t1/ι(2)0 < t \le 1/\iota(2), and put x:=t2x := t^{2} and y:=ι(4)t2y := \iota(4)t^{2}. Then 0<xy=ι(4)t2ι(4)/ι(4)=10 < x \le y = \iota(4)t^{2} \le \iota(4)/\iota(4) = 1, so x,yIx, y \in I; and s(x)=ts(x) = t and s(y)=ι(2)ts(y) = \iota(2)t by [L3], since t0t \ge 0 with t2=xt^{2} = x and ι(2)t0\iota(2)t \ge 0 with (ι(2)t)2=ι(4)t2=y(\iota(2)t)^{2} = \iota(4)t^{2} = y. Hence s(y)s(x)=ι(2)tt=t|s(y)-s(x)| = \iota(2)t - t = t and yx=ι(3)t2|y - x| = \iota(3)t^{2} by [L6], and the supposition gives tLι(3)t2t \le L\,\iota(3)t^{2}; dividing by t>0t > 0 gives 1ι(3)Lt1 \le \iota(3)Lt for every such tt. Taking t:=1/ι(2)t := 1/\iota(2) shows ι(3)L/ι(2)1\iota(3)L/\iota(2) \ge 1, so L>0L > 0. Now use [L5] to fix a natural m1m \ge 1 with 1/ι(m)<1/(ι(3)L)1/\iota(m) < 1/(\iota(3)L) and put t:=min{1/ι(m), 1/ι(2)}t := \min\{1/\iota(m),\ 1/\iota(2)\}, a real with 0<t1/ι(2)0 < t \le 1/\iota(2); then ι(3)Ltι(3)L/ι(m)<1\iota(3)Lt \le \iota(3)L/\iota(m) < 1, contradicting 1ι(3)Lt1 \le \iota(3)Lt. So no such LL exists.

step 1.1L3L4L5L6
3.1

The refuted claim therefore fails at I:=(0,1]I := (0,1] and h:=sh := s: by step 1.1 the function ss is continuous on the order-convex set II and differentiable at every point of II, in particular at every interior point of II by step 1.2, and yet by step 2.2 it is not Lipschitz on II. Nothing in [L8] is contradicted: by step 2.1 no real MM bounds s|s'| on the interior of II, so the hypothesis deleted from that corollary is exactly the one that fails.

step 1.1step 1.2step 2.1step 2.2L8

Remarks

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

With f(x)=x3f(x) = x^{3} and g(x)=x2g(x) = x^{2} on [1,1][-1,1] the quotient form f(b)f(a)g(b)g(a)=f(c)g(c)\frac{f(b)-f(a)}{g(b)-g(a)} = \frac{f'(c)}{g'(c)} is meaningless because g(b)=g(a)g(b) = g(a), while the product form of Cauchy's theorem still holds

Statement refuted

Refuted claim: let a,bRa, b \in \mathbb{R} with a<ba < b and let f,g:[a,b]Rf, g : [a,b] \to \mathbb{R} be continuous on [a,b][a,b] (Continuity of f:ARf : A \to \mathbb{R} at a point of AA and on AA: the ε\varepsilon-δ\delta condition, its agreement with limxcf(x)=f(c)\lim_{x \to c} f(x) = f(c) at a limit point, and continuity at an isolated point) and differentiable at every point of (a,b)(a,b) (The derivative f(c)=limxcf(x)f(c)xcf'(c) = \lim_{x \to c} \frac{f(x) - f(c)}{x - c} of f:ARf : A \to \mathbb{R} at a point cAc \in A that is a limit point of AA, and differentiability on a set). Then there is c(a,b)c \in (a,b) with

f(b)f(a)g(b)g(a)  =  f(c)g(c).\frac{f(b)-f(a)}{g(b)-g(a)} \;=\; \frac{f'(c)}{g'(c)} .

This is the shape in which Cauchy's mean value theorem is usually remembered, and it is not what 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 \in (a,b) with (f(b)f(a))g(c)=(g(b)g(a))f(c)\bigl(f(b)-f(a)\bigr)g'(c) = \bigl(g(b)-g(a)\bigr)f'(c); no hypothesis on gg' is needed in this product form says. It is false as stated, because under the hypotheses given neither quotient need be a real number at all. The witness below makes both denominators vanish.

Facts & Assumptions

Given: The reals a:=1a := -1 and b:=1b := 1 and the functions f,g:[1,1]Rf, g : [-1,1] \to \mathbb{R} with f(x):=x3f(x) := x^{3} and g(x):=x2g(x) := x^{2} (Integer powers ama^m, Intervals of R\mathbb{R}: the nine order-convex forms, nondegeneracy, and length); numerals denote canonical naturals (The canonical natural ι(n)=n1F\iota(n) = n \cdot 1_F of a field).

[L3]

Cauchy's mean value theorem (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 \in (a,b) with (f(b)f(a))g(c)=(g(b)g(a))f(c)\bigl(f(b)-f(a)\bigr)g'(c) = \bigl(g(b)-g(a)\bigr)f'(c); no hypothesis on gg' is needed in this product form), in its product form: under the hypotheses above there is c(a,b)c \in (a,b) with (f(b)f(a))g(c)=(g(b)g(a))f(c)\bigl(f(b)-f(a)\bigr)g'(c) = \bigl(g(b)-g(a)\bigr)f'(c).

[L4]

Rolle's theorem (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 \in (a,b)): a function continuous on [a,b][a,b], differentiable at every point of (a,b)(a,b) and taking equal values at the endpoints has a vanishing derivative somewhere in (a,b)(a,b).

[L5]

Signs and powers (Integer powers ama^m, Sign rules for products and monotonicity of multiplication, Monotonicity of xxnx \mapsto x^n and of nann \mapsto a^n): the recursion an+1=anaa^{n+1} = a^{n}a with a0=1a^{0} = 1 gives (1)2=(1)(1)=1(-1)^{2} = (-1)(-1) = 1, the product of two negatives being positive (Sign rules for products and monotonicity of multiplication), and (1)3=(1)2(1)=1(-1)^{3} = (-1)^{2}(-1) = -1; that 1n=11^{n} = 1 for every natural nn is claim 4 of Monotonicity of xxnx \mapsto x^n and of nann \mapsto a^n and is not read off Integer powers ama^m.

[L6]

Canonical naturals (The canonical natural ι(n)=n1F\iota(n) = n \cdot 1_F of a field, Canonical naturals are positive and strictly increasing): ι(1)=1\iota(1) = 1, ι(m+n)=ι(m)+ι(n)\iota(m+n) = \iota(m)+\iota(n) and ι(mn)=ι(m)ι(n)\iota(mn) = \iota(m)\iota(n) for m,n1m, n \ge 1; in particular ι(2)ι(2)=ι(4)>0\iota(2)\iota(2) = \iota(4) > 0, so ι(4)0\iota(4) \ne 0.

[L7]

Division by 00 is not defined: 00 has no multiplicative inverse in a field (Field).

Counterexample

technique · direct
1.1

By [L2] both ff and gg are continuous on [1,1][-1,1], and by [L1] both are differentiable at every c[1,1]c \in [-1,1], with f(c)=ι(3)c2f'(c) = \iota(3)c^{2} and g(c)=ι(2)c1=ι(2)cg'(c) = \iota(2)c^{1} = \iota(2)c, using [L5] for c1=cc^{1} = c. So the pair (f,g)(f,g) satisfies every hypothesis of the refuted claim, and of [L3], with a=1a = -1 and b=1b = 1.

L1L2L5
1.2

By [L5], f(1)=1f(1) = 1, f(1)=1f(-1) = -1, g(1)=1g(1) = 1 and g(1)=1g(-1) = 1. Hence f(b)f(a)=1(1)=ι(2)f(b)-f(a) = 1 - (-1) = \iota(2) and g(b)g(a)=11=0g(b)-g(a) = 1 - 1 = 0.

L5L6
2.1

The left-hand side of the refuted claim names no real number: its denominator g(b)g(a)g(b)-g(a) is 00 by step 1.2, and 00 has no inverse by [L7]. So there is no cc for which the asserted equation holds, since the equation cannot even be formed; the claim fails on this pair.

step 1.2L7
2.2

The right-hand side fails as well at one point of the interval: g(0)=ι(2)0=0g'(0) = \iota(2) \cdot 0 = 0 by step 1.1, so the quotient f(c)/g(c)f'(c)/g'(c) is undefined at c=0c = 0, again by [L7].

step 1.1L7
2.3

The product form is untouched. By [L3] there is c(1,1)c \in (-1,1) with (f(b)f(a))g(c)=(g(b)g(a))f(c)\bigl(f(b)-f(a)\bigr)g'(c) = \bigl(g(b)-g(a)\bigr)f'(c), which by steps 1.1 and 1.2 reads ι(2)ι(2)c=0ι(3)c2\iota(2)\,\iota(2)c = 0 \cdot \iota(3)c^{2}, that is ι(4)c=0\iota(4)c = 0; since ι(4)0\iota(4) \ne 0 by [L6], this forces c=0c = 0. And c=0c = 0 does lie in (1,1)(-1,1) and does satisfy the identity, both sides being 00. So [L3] holds on this pair, with c=0c = 0 its only admissible point.

step 1.1step 1.2L3L6
3.1

The vanishing of g(b)g(a)g(b)-g(a) is not an accident of the choice. By step 1.2 one has g(1)=g(1)g(-1) = g(1), so [L4] already forces gg' to vanish at some point of (1,1)(-1,1), and by step 2.3 that point is c=0c = 0, the same point the product form produces. So on this pair every quotient the refuted claim writes down is undefined, while [L3] is satisfied; the quotient form needs hypotheses the product form does not, and as stated it is false.

step 2.1step 2.2step 2.3L4

Remarks

Sources