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

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.

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]

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

Depends on

Used by

Dependency tree · two levels

34 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

Monotonic function (Wikipedia) (standard reference, not scraped)
Mean value theorem (Wikipedia) (standard reference, not scraped)
W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 5 (Thm 5.11) (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)