Alphabeta Math
CorollaryStatement: 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.

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⊆R be order-convex (Intervals of R: the nine order-convex forms, nondegeneracy, and length) and let f:I→R be continuous on I (Continuity of f:A→R at a point of A and on A: the ε-δ condition, its agreement with lim⁡x→cf(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→cf(x)−f(c)x−c of f:A→R at a point c∈A that is a limit point of A, and differentiability on a set), with

f′(x)=0at every interior point x of I.

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

Consequently, if f,g:I→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)+kfor every x∈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]⊆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⊆R and a function f:I→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∈(a,b) with f(b)−f(a)=f′(c)(b−a)): for u<v and h:[u,v]→R continuous on [u,v] and differentiable at every point of (u,v), there is c∈(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∈I and u≤z≤v then z∈I; so u,v∈I with u≤v gives [u,v]⊆I.

[L3]

For u<v in I and x∈(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)⊆(u,v)⊆[u,v]⊆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→cf(x)−f(c)x−c of f:A→R at a point c∈A that is a limit point of A, and differentiability on a set): if B⊆A, if p∈B is a limit point of B and if h:A→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→cf(x)−f(c)x−c of f:A→R at a point c∈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⊆A and h:A→R is continuous at p∈B, then h∣B is continuous at p (Continuity of f:A→R at a point of A and on A: the ε-δ condition, its agreement with lim⁡x→cf(x)=f(c) at a limit point, and continuity at an isolated point).

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∈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∈(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∈(u,v) with f(v)−f(u)=(f∣[u,v])′(c) (v−u)=0⋅(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∈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.

Depends on

Used by

Dependency tree · two levels

32 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