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.

✓ 9 results · all verified · 0 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 9 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

The Fundamental Theorems of Calculus

1 · Prerequisites

2 · Summary

bounded-variation-and-riemann-stieltjes supplies Riemann--Stieltjes integration and its reduction to an ordinary Riemann integral for a continuously differentiable integrator. uniform-convergence-of-functions supplies the uniform integral estimate used to pass a parameter derivative through an integral. sine-cosine-and-the-definition-of-pi supplies the derivative, bounds, and special values used in the oscillatory examples. The working first and second fundamental theorems already identify the derivative of an integral function at continuity points and evaluate an integrable derivative on a closed interval.

The development first separates the pointwise and almost-everywhere forms of the first theorem, then proves Newton--Leibniz with only an interior derivative and extends it across finite and countable exceptional sets. Integration by parts, substitution, one-sided differentiation, and differentiation under the integral sign follow with their endpoint and integrability hypotheses explicit. The closing theorem transfers both fundamental-theorem forms to continuously differentiable Riemann--Stieltjes integrators.

3 · Logical flowchart

4 · Definitions, theorems and proofs

RemarkRemark: AI-adaptedProof: Not applicableaudited 2026-08-13Open item page →

Roadmap through the three strengths of FTC I and the five Riemann strengths of FTC II

Remark

There are three progressively broader Riemann forms of the first fundamental theorem. The continuous-integrand form says that the integral function is differentiable everywhere. The pointwise form The first fundamental theorem: if $f$ is integrable on $[a, b]$ and continuous at $c$ , then $F^{'} (c) = f (c)$ ; in particular a continuous $f$ has $F$ as a primitive needs continuity only at the point where the derivative is taken. The almost-everywhere consequence on this page combines that pointwise theorem with the Riemann integrability criterion; the later Lebesgue theory gives the corresponding absolutely-continuous formulation.

For Newton--Leibniz, the continuously differentiable working form is contained in The second fundamental theorem: if $G$ is differentiable on $[a, b]$ with $G^{'} = f$ and $f$ is integrable, then $\int_{a}^{b} f = G (b) - G (a)$ , whose published statement already allows an arbitrary integrable derivative on the closed interval. This page successively removes endpoint differentiability, permits finitely many exceptional interior points, and then permits a countable exceptional set by Botsko's theorem. The later absolutely-continuous theorem is stronger in a different direction and is not used here.

CorollaryStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-08-13Open item page →

Assuming Countable Choice, the integral function of a Riemann-integrable function is Lipschitz and differentiable almost everywhere, with derivative equal to the integrand there

Statement

Assume the Axiom of Countable Choice. Let $a < b$ , let $f : [a, b] \to R$ be Riemann integrable, and let

$F (x) : = \int_{a}^{x} f .$

Then $F$ is Lipschitz on $[a, b]$ . If $D$ is the set of discontinuities of $f$ , then $D$ has measure zero and

$F^{'} (x) = f (x) (x \in [a, b] ∖ D) .$

Thus the set of points where $F^{'}$ fails to exist or differs from $f$ is contained in a set of measure zero. At $a$ and $b$ , the displayed derivative is the relative one-sided derivative on $[a, b]$ .

Facts & Assumptions

Given: Reals $a < b$ , an integrable $f : [a, b] \to R$ , its integral function $F$ , and Countable Choice.

[L1]

An integrable $f$ is bounded, and if $∣ f ∣ \leq K$ then its integral function satisfies $∣ F (y) - F (x) ∣ \leq K ∣ y - x ∣$ (The integral function of a bounded integrable $f$ is Lipschitz, hence uniformly continuous).

[L2]

Assuming Countable Choice, a bounded function is Riemann integrable if and only if its discontinuity set has measure zero (Lebesgue's criterion for Riemann integrability: a bounded $f$ on $[a, b]$ is Riemann integrable if and only if its set of discontinuities has measure zero).

[L3]

If $f$ is integrable and continuous at $c \in [a, b]$ , then its integral function is differentiable at $c$ and $F^{'} (c) = f (c)$ , with relative endpoint derivatives (The first fundamental theorem: if $f$ is integrable on $[a, b]$ and continuous at $c$ , then $F^{'} (c) = f (c)$ ; in particular a continuous $f$ has $F$ as a primitive).

Proof

technique · direct

1.1

Integrability supplies a bound $∣ f ∣ \leq K$ , so $F$ is Lipschitz by [L1].

givenL1

1.2

The discontinuity set $D$ has measure zero by the forward implication of [L2], whose stated proof is the sole use of Countable Choice.

givenL2

2.1

Every $x \in [a, b] ∖ D$ is a continuity point of $f$ , so [L3] gives $F^{'} (x) = f (x)$ there, including the relative derivative at an endpoint outside $D$ .

step 1.2L3

3.1

Hence every point at which the derivative conclusion fails lies in $D$ , and that containing set has measure zero.

step 1.2step 2.1∎

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-13Open item page →

Newton–Leibniz needs only continuity on $[a, b]$ , differentiability on $(a, b)$ , and a Riemann-integrable extension of the interior derivative

Statement

Let $a < b$ . Suppose $G : [a, b] \to R$ is continuous on $[a, b]$ and differentiable on $(a, b)$ . If $f : [a, b] \to R$ is Riemann integrable and

$f (x) = G^{'} (x) (a < x < b),$

then

$\int_{a}^{b} f = G (b) - G (a) .$

No derivative of $G$ at either endpoint is assumed, and the two endpoint values assigned to the integrable extension $f$ do not enter the conclusion.

Facts & Assumptions

Given: Reals $a < b$ , a continuous $G : [a, b] \to R$ differentiable on $(a, b)$ , and an integrable $f$ agreeing there with $G^{'}$ .

[L1]

If a function is continuous on $[u, v]$ and differentiable on $(u, v)$ , then some $ξ \in (u, v)$ satisfies $G (v) - G (u) = G^{'} (ξ) (v - u)$ (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)$ ).

[L2]

For a partition $P = (t_{0}, \dots, t_{m})$ , the lower and upper Darboux sums are obtained by multiplying each subinterval length by the infimum and supremum of $f$ there (Partition of $[a, b]$ as a finite strictly increasing list $a = t_{0} < t_{1} < \dots < t_{n} = b$ , its subintervals and their lengths, its mesh, refinement, and the common refinement of two partitions, The lower and upper Darboux integrals of a bounded $f$ on $[a, b]$ as $\sup_{P} L (f, P)$ and $\inf_{P} U (f, P)$ , Darboux integrability as their equality, and the notation $\int_{a}^{b} f$ ).

[L3]

If $f$ is integrable with integral $I$ , then every lower sum is at most $I$ and every upper sum is at least $I$ (The lower and upper Darboux integrals of a bounded $f$ on $[a, b]$ as $\sup_{P} L (f, P)$ and $\inf_{P} U (f, P)$ , Darboux integrability as their equality, and the notation $\int_{a}^{b} f$ ).

Proof

technique · squeeze

1.1

Fix a partition $P = (t_{0}, \dots, t_{m})$ of $[a, b]$ . For each $i < m$ , [L1] gives $ξ_{i} \in (t_{i}, t_{i + 1})$ such that $G (t_{i + 1}) - G (t_{i}) = f (ξ_{i}) (t_{i + 1} - t_{i})$ .

givenL1

2.1

If $m_{i}$ and $M_{i}$ are the infimum and supremum of $f$ on $[t_{i}, t_{i + 1}]$ , then $m_{i} (t_{i + 1} - t_{i}) \leq G (t_{i + 1}) - G (t_{i}) \leq M_{i} (t_{i + 1} - t_{i})$ .

step 1.1L2

3.1

Summing step 2.1 and telescoping the increments of $G$ gives $L (f, P) \leq G (b) - G (a) \leq U (f, P)$ .

step 2.1L2

4.1

Taking the supremum of the lower sums and the infimum of the upper sums, which coincide because $f$ is integrable, yields $\int_{a}^{b} f = G (b) - G (a)$ .

step 3.1L3

5.1

Every $ξ_{i}$ lies in an open subinterval, so neither endpoint derivative nor either endpoint value of $f$ was used.

step 1.1∎

CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-13Open item page →

Newton–Leibniz remains valid across finitely many exceptional interior points when the primitive is continuous

Statement

Let $a < b$ , let $E \subseteq [a, b]$ be finite, and let $G : [a, b] \to R$ be continuous. Suppose $G$ is differentiable at every point of $(a, b) ∖ E$ , and let $f : [a, b] \to R$ be Riemann integrable with

$f (x) = G^{'} (x) (x \in (a, b) ∖ E) .$

Then

$\int_{a}^{b} f = G (b) - G (a) .$

Points of $E$ equal to $a$ or $b$ impose no additional condition, because the hypothesis concerns only interior derivatives.

Facts & Assumptions

Given: The data in the statement.

[L1]

If a continuous function on a closed interval is differentiable in its interior and its interior derivative has an integrable extension, the extension integrates to the endpoint change (Newton–Leibniz needs only continuity on $[a, b]$ , differentiability on $(a, b)$ , and a Riemann-integrable extension of the interior derivative).

[L2]

An integrable function restricts to closed subintervals, and its integral is additive over finitely many adjacent subintervals (For $a < c < b$ : $f$ is integrable on $[a, b]$ if and only if it is integrable on $[a, c]$ and on $[c, b]$ , and then $\int_{a}^{b} f = \int_{a}^{c} f + \int_{c}^{b} f$ ; with the oriented form for arbitrary $a, b, c$ ).

Proof

technique · decomposition

1.1

List the distinct points of $E \cap (a, b)$ in increasing order as $e_{1} < \dots < e_{m}$ ; if this set is empty, take $m = 0$ . Put $e_{0} = a$ and $e_{m + 1} = b$ .

givenchoose

1.2

On every $[e_{i}, e_{i + 1}]$ , the restriction of $G$ is continuous and differentiable throughout the open subinterval, while the restriction of $f$ is integrable and agrees there with $G^{'}$ .

givenL2

2.1

Applying [L1] on each subinterval gives $\int_{e_{i}}^{e_{i + 1}} f = G (e_{i + 1}) - G (e_{i})$ .

step 1.2L1

3.1

Summing step 2.1, using [L2], and telescoping yields $\int_{a}^{b} f = G (b) - G (a)$ .

step 2.1L2

4.1

When $m = 0$ there is one subinterval and the proof is exactly [L1]; endpoint members of $E$ never occur in an open subinterval.

step 1.1step 2.1∎

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-13Open item page →

Botsko's theorem: if $F$ is continuous on $[a, b]$ , $F^{'} (x) = f (x)$ off a countable subset of $(a, b)$ , and $f$ is Riemann integrable, then $\int_{a}^{b} f = F (b) - F (a)$

Statement

Let $a < b$ , let $E \subseteq (a, b)$ be at most countable, let $F : [a, b] \to R$ be continuous, and let $f : [a, b] \to R$ be Riemann integrable. If $F$ is differentiable at every $x \in (a, b) ∖ E$ and

$F^{'} (x) = f (x) (x \in (a, b) ∖ E),$

then

$\int_{a}^{b} f = F (b) - F (a) .$

Neither derivatives at the endpoints nor derivatives at points of $E$ are required.

Facts & Assumptions

Given: The data in the statement.

[L1]

An at-most-countable set is empty or, when nonempty, is the range of a surjection $e : N \to E$ ; repetitions are allowed and no choice is required (Finite, countably infinite, countable, uncountable, A nonempty set is at most countable iff it is a surjective image of $N$ ).

[L2]

Continuity at $c$ means that every prescribed positive error bounds $∣ H (x) - H (c) ∣$ throughout some neighbourhood of $c$ (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).

[L3]

Differentiability at $x$ means that the difference quotients $(H (y) - H (x)) / (y - x)$ tend to $H^{'} (x)$ as $y \to x$ (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).

[L4]

A nested sequence of nonempty closed bounded intervals whose lengths tend to $0$ has a one-point intersection (A nested sequence of nonempty closed bounded intervals has nonempty intersection, and the intersection is a single point exactly when the lengths tend to $0$ ).

[L5]

The geometric sequence $2^{- n}$ tends to $0$ (For $∣ r ∣ < 1$ the sequence $r^{k}$ is null, and for $∣ r ∣ > 1$ the sequence $∣ r ∣^{k}$ diverges to $+ \infty$ ).

[L6]

For a partition $P$ , the lower and upper Darboux sums use the infima and suprema on its subintervals, and an integrable function has its integral between every such pair of sums (For bounded $f$ on $[a, b]$ and a partition $P$ : the infimum $m_{i}$ and supremum $M_{i}$ of $f$ on the $i$ -th subinterval, and the lower and upper Darboux sums $L (f, P) = \sum_{i} m_{i} Δ_{i}$ and $U (f, P) = \sum_{i} M_{i} Δ_{i}$ , The lower and upper Darboux integrals of a bounded $f$ on $[a, b]$ as $\sup_{P} L (f, P)$ and $\inf_{P} U (f, P)$ , Darboux integrability as their equality, and the notation $\int_{a}^{b} f$ , Partition of $[a, b]$ as a finite strictly increasing list $a = t_{0} < t_{1} < \dots < t_{n} = b$ , its subintervals and their lengths, its mesh, refinement, and the common refinement of two partitions).

Proof

technique · squeeze

1.1

It suffices first to prove the countable-exception monotonicity lemma: if $H : [u, v] \to R$ is continuous and $H^{'} (x) \leq 0$ on $(u, v) ∖ E$ , where $E$ is at most countable, then $H (v) \leq H (u)$ .

givensuffices

1.2

Suppose contrariwise that $H (v) > H (u)$ . By continuity choose $u < p < q < v$ with $H (q) > H (p)$ , and put $c = (H (q) - H (p)) / (q - p) > 0$ .

givenL2algebra

1.3

If $E$ is nonempty, fix the surjection $e : N \to E$ from [L1]; if $E$ is empty, put $e_{n} = u$ for every $n$ . Assign stage $n$ the slope-loss budget $δ_{n} = c 2^{- n - 2}$ . The finite geometric-sum identity gives $\sum_{j \leq n} δ_{j} < c / 2$ for every $n$ .

L1algebra

1.4

Fix a partition $P = (t_{0}, \dots, t_{m})$ and let $m_{i}, M_{i}$ be the infimum and supremum of $f$ on $[t_{i}, t_{i + 1}]$ . Off $E$ , the functions $F (x) - M_{i} x$ and $m_{i} x - F (x)$ have derivatives at most $0$ .

givenL6algebra

2.1

Construct nested closed intervals $I_{n} = [p_{n}, q_{n}] \subseteq [p, q]$ . Start with $I_{0} = [p, q]$ . Given $I_{n}$ , one of its two closed halves has secant slope at least the slope of $I_{n}$ , because the latter is the length-weighted average of the two half-slopes. Call that half $J$ . If $e_{n} \notin J$ , take $I_{n + 1} = J$ . If $e_{n} \in J$ , split $J$ at $e_{n}$ ; one nondegenerate side has slope at least the slope of $J$ , and [L2] lets us move its endpoint $e_{n}$ slightly into that side so that the resulting closed interval excludes $e_{n}$ and loses less than $δ_{n}$ in slope. Thus $I_{n + 1} \subseteq I_{n}$ , $∣ I_{n + 1} ∣ \leq ∣ I_{n} ∣ / 2$ , $e_{n} \notin I_{n + 1}$ , and its secant slope is at least $c - \sum_{j \leq n} δ_{j} \geq c / 2$ .

step 1.2step 1.3L2algebra

3.1

By step 2.1 and [L5], the nested intervals have lengths tending to $0$ , so [L4] gives a unique $x$ in their intersection. The initial interval lies in $(u, v)$ , and $x \neq e_{n}$ for every $n$ ; hence $x \in (u, v) ∖ E$ .

step 2.1L1L4L5

4.1

Write $I_{n} = [p_{n}, q_{n}]$ . Both endpoints tend to $x$ . The secant slope on $I_{n}$ is a convex combination of the two difference quotients based at $x$ (omitting a zero-length side), so [L3] makes those slopes tend to $H^{'} (x)$ . Step 2.1 keeps every slope at least $c / 2$ , whence $H^{'} (x) \geq c / 2 > 0$ , contradicting the hypothesis. Therefore $H (v) \leq H (u)$ and the monotonicity lemma is proved.

step 2.1step 3.1L3algebradischarge-contradiction

5.1

Apply the lemma from step 4.1 on $[t_{i}, t_{i + 1}]$ to obtain $m_{i} (t_{i + 1} - t_{i}) \leq F (t_{i + 1}) - F (t_{i}) \leq M_{i} (t_{i + 1} - t_{i})$ .

step 4.1step 1.4

6.1

Summing step 5.1 and telescoping yields $L (f, P) \leq F (b) - F (a) \leq U (f, P)$ .

step 5.1L6

7.1

Since $f$ is integrable, the supremum of all lower sums and the infimum of all upper sums are both $\int_{a}^{b} f$ ; step 6.1 therefore forces $\int_{a}^{b} f = F (b) - F (a)$ .

step 6.1L6∎

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-08-13Open item page →

Integration by parts for continuous factors with Riemann-integrable extensions of their interior derivatives

Statement

Let $a < b$ . Let $F, G : [a, b] \to R$ be continuous on $[a, b]$ and differentiable on $(a, b)$ . Suppose $f, g : [a, b] \to R$ are Riemann integrable and agree on $(a, b)$ with $F^{'}$ and $G^{'}$ , respectively. Then $F g$ and $f G$ are Riemann integrable and

$\int_{a}^{b} F (x) g (x) d x + \int_{a}^{b} f (x) G (x) d x = F (b) G (b) - F (a) G (a) .$

Equivalently,

$\int_{a}^{b} F g = [F G]_{a}^{b} - \int_{a}^{b} f G .$

No endpoint derivative of either factor is assumed.

Facts & Assumptions

Given: The functions in the statement.

[L1]

The product rule gives $(F G)^{'} = F^{'} G + F G^{'}$ wherever both derivatives exist (Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ ).

[L2]

Continuous functions on a compact interval are Riemann integrable, and products of Riemann-integrable functions are Riemann integrable (A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion, If $f, g$ are integrable on $[a, b]$ then so are $∣ f ∣$ , $f^{2}$ , $f g$ , $\max (f, g)$ and $\min (f, g)$ , and $∣ \int_{a}^{b} f ∣ \leq \int_{a}^{b} ∣ f ∣$ ).

[L3]

The integral is linear on Riemann-integrable functions (Integrable functions on $[a, b]$ form a set closed under sums and scalar multiples, and $\int_{a}^{b} (λ f + μ g) = λ \int_{a}^{b} f + μ \int_{a}^{b} g$ ).

[L4]

A continuous function with an interior derivative admitting an integrable extension satisfies Newton--Leibniz (Newton–Leibniz needs only continuity on $[a, b]$ , differentiability on $(a, b)$ , and a Riemann-integrable extension of the interior derivative).

Proof

technique · direct

1.1

The functions $F$ and $G$ are integrable, so [L2] makes $f G$ and $F g$ integrable; their sum $h : = f G + F g$ is integrable as well.

givenL2L3

1.2

The product $F G$ is continuous on $[a, b]$ , differentiable on $(a, b)$ , and [L1] gives $(F G)^{'} = f G + F g = h$ throughout the interior.

givenL1

2.1

Apply [L4] to $F G$ and its integrable derivative extension $h$ to obtain $\int_{a}^{b} h = F (b) G (b) - F (a) G (a)$ .

step 1.1step 1.2L4

3.1

Expanding the left side by [L3] gives the first displayed identity, and subtraction gives the equivalent form.

step 2.1L3algebra∎

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-08-13Open item page →

Substitution for a continuous inner map with a Riemann-integrable extension of its interior derivative, without monotonicity or injectivity

Statement

Let $c < d$ , let $J = [p, q]$ with $p < q$ , and let $f : J \to R$ be continuous. Suppose $φ : [c, d] \to J$ is continuous on $[c, d]$ and differentiable on $(c, d)$ , and that the interior derivative has a Riemann-integrable extension $h : [c, d] \to R$ . Then $(f \circ φ) h$ is Riemann integrable and

$\int_{c}^{d} f (φ (t)) h (t) d t = \int_{φ (c)}^{φ (d)} f (x) d x .$

The limits on the right are oriented. No injectivity or monotonicity of $φ$ is required; the identity also covers $φ (c) > φ (d)$ and $φ (c) = φ (d)$ .

Facts & Assumptions

Given: The functions and intervals in the statement.

[L1]

A continuous integrand has an integral function differentiable at every point, with derivative equal to that integrand (The first fundamental theorem: if $f$ is integrable on $[a, b]$ and continuous at $c$ , then $F^{'} (c) = f (c)$ ; in particular a continuous $f$ has $F$ as a primitive).

[L2]

The chain rule gives $(H \circ φ)^{'} = (H^{'} \circ φ) φ^{'}$ on the interior (The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g (c)$ , then $f \circ g$ is differentiable at $c$ with $(f \circ g)^{'} (c) = f^{'} (g (c)) g^{'} (c)$ ).

[L3]

[L4]

[L5]

Oriented integrals satisfy $\int_{u}^{u} f = 0$ and $\int_{v}^{u} f = - \int_{u}^{v} f$ (The integral with oriented limits: $\int_{a}^{a} f : = 0$ and $\int_{b}^{a} f : = - \int_{a}^{b} f$ ).

Proof

technique · reduction

1.1

Fix $r \in J$ and define $H (x) : = \int_{r}^{x} f$ with oriented limits. By [L1], $H$ is differentiable on $J$ and $H^{'} = f$ , including relative endpoint derivatives.

givenL1L5

1.2

The composite $f \circ φ$ is continuous and hence integrable; its product with the integrable $h$ is integrable by [L3].

givenL3

2.1

The composite $H \circ φ$ is continuous on $[c, d]$ , differentiable on $(c, d)$ , and [L2] gives $(H \circ φ)^{'} (t) = f (φ (t)) h (t)$ there.

givenstep 1.1L2

3.1

Applying [L4] to $H \circ φ$ gives $\int_{c}^{d} (f \circ φ) h = H (φ (d)) - H (φ (c))$ .

step 2.1step 1.2L4

4.1

The oriented definition in [L5] gives $H (v) - H (u) = \int_{u}^{v} f$ for every $u, v \in J$ , whether $u < v$ , $u = v$ , or $u > v$ . Taking $u = φ (c)$ and $v = φ (d)$ completes all three endpoint-order cases.

step 1.1L5algebra∎

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-13Open item page →

For an integrable $f$ , the one-sided derivatives of $F (x) = \int_{a}^{x} f$ equal the corresponding one-sided limits of $f$ ; at a jump they are unequal

Statement

Let $a < b$ , let $f : [a, b] \to R$ be Riemann integrable, and put $F (x) = \int_{a}^{x} f$ .

If $c \in [a, b)$ and $\lim_{x \to c^{+}} f (x) = L_{+}$ , then the right derivative exists and $F_{+}^{'} (c) = L_{+}$ .
If $c \in (a, b]$ and $\lim_{x \to c^{-}} f (x) = L_{-}$ , then the left derivative exists and $F_{-}^{'} (c) = L_{-}$ .

In particular, if both one-sided limits exist at an interior point and are unequal, then $F$ is not differentiable there. The value $f (c)$ itself is irrelevant to both conclusions.

Facts & Assumptions

Given: The integrable $f$ , its integral function $F$ , and the indicated one-sided limits.

[L1]

Integral additivity gives $F (y) - F (c) = \int_{c}^{y} f$ for all $c, y \in [a, b]$ , with oriented limits (The integral function $F (x) : = \int_{a}^{x} f$ of an integrable $f$ , For $a < c < b$ : $f$ is integrable on $[a, b]$ if and only if it is integrable on $[a, c]$ and on $[c, b]$ , and then $\int_{a}^{b} f = \int_{a}^{c} f + \int_{c}^{b} f$ ; with the oriented form for arbitrary $a, b, c$ ).

[L2]

The right-limit condition says that for every $ε > 0$ , $∣ f (x) - L_{+} ∣ < ε$ throughout a sufficiently short interval to the right of $c$ ; the left version is analogous (The left and right limits of $f$ at $c$ , as limits of the restrictions of $f$ to $A \cap (- \infty, c)$ and $A \cap (c, \infty)$ ).

[L3]

If $∣ g ∣ \leq M$ on an interval of length $ℓ$ , then $∣ \int g ∣ \leq M ℓ$ (If $m \leq f \leq M$ on $[a, b]$ then $m (b - a) \leq L (f, P) \leq \underline{\int_{a}^{b}} f \leq \overline{\int_{a}^{b}} f \leq U (f, P) \leq M (b - a)$ for every partition $P$ ; in particular every constant function is integrable, with $\int_{a}^{b} c = c (b - a)$ ).

Proof

technique · epsilon-delta

1.1

Assume the right limit exists and fix $ε > 0$ . By [L2], choose $δ > 0$ so that $∣ f (x) - L_{+} ∣ < ε$ whenever $c < x < c + δ$ within $[a, b]$ .

givenL2

1.2

For the left limit, take $h < 0$ , rewrite the same quotient using the oriented integral over $[c + h, c]$ , and apply [L2] and [L3]; its limit is $L_{-}$ .

givenL1L2L3

2.1

For $0 < h < δ$ with $c + h \leq b$ , [L1] and linearity give $\frac{F (c + h) - F (c)}{h} - L_{+} = \frac{1}{h} \int_{c}^{c + h} (f - L_{+})$ .

step 1.1L1algebra

3.1

By [L3], the absolute value in step 2.1 is at most $ε$ . Hence the right difference quotient tends to $L_{+}$ .

step 1.1step 2.1L3

4.1

At an interior point a two-sided derivative would have to equal both one-sided derivatives, so unequal $L_{+}$ and $L_{-}$ preclude it. Neither estimate refers to $f (c)$ .

step 3.1step 1.2∎

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-13Open item page →

Leibniz's rule on a compact rectangle: an interior parameter derivative with a continuous extension may be passed through a Riemann integral

Statement

Let $a < b$ and $c < d$ . Suppose $g, h : [a, b] \times [c, d] \to R$ are continuous and, for every fixed $t \in [c, d]$ , the function $x \mapsto g (x, t)$ is differentiable on $(a, b)$ with derivative $h (x, t)$ . Define

$G (x) : = \int_{c}^{d} g (x, t) d t .$

Then $G$ is differentiable on $[a, b]$ as a function on that interval and

$G^{'} (x) = \int_{c}^{d} h (x, t) d t (x \in [a, b]) .$

At $a$ and $b$ the derivative is relative and one-sided. The derivative hypothesis is imposed only for interior parameter values; continuity of $h$ supplies its endpoint values.

Facts & Assumptions

Given: The rectangle and functions in the statement.

[L1]

A continuous real function on a compact interval is bounded and Riemann integrable (A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion).

[L2]

A closed rectangle in $R^{2}$ is compact, and a continuous map from a compact metric space to $R$ is uniformly continuous (Heine-Borel in $R^{n}$ : with the Euclidean metric a subset of $R^{n}$ is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line, Heine-Cantor: a continuous map from a compact metric space to any metric space is uniformly continuous).

[L3]

The mean value theorem turns a difference quotient into a derivative value at an intermediate point (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)$ ).

[L4]

If two integrable functions differ uniformly by at most $η$ , then their integrals over $[c, d]$ differ by at most $η (d - c)$ (Uniformly close integrable functions have integrals differing by at most the interval length times their uniform error).

[L5]

Relative differentiability on a closed interval is convergence of the difference quotient over points of that interval (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).

Proof

technique · epsilon-delta

1.1

For each $x$ , the slice $t \mapsto g (x, t)$ is continuous, so [L1] makes $G (x)$ well defined; the same applies to every slice of $h$ .

givenL1

1.2

Fix $x \in [a, b]$ and $ε > 0$ . Uniform continuity of $h$ on the compact rectangle gives $δ > 0$ such that $∣ h (y, t) - h (x, t) ∣ < ε / (d - c)$ whenever $∣ y - x ∣ < δ$ , uniformly in $t$ .

givenL2

2.1

Let $y \in [a, b]$ , $0 < ∣ y - x ∣ < δ$ . For every $t$ , [L3] applied to the parameter slice on the interval with endpoints $x, y$ gives a point $ξ_{t}$ strictly between them with $\frac{g (y, t) - g (x, t)}{y - x} = h (ξ_{t}, t)$ .

step 1.2L3

3.1

Because $∣ ξ_{t} - x ∣ < ∣ y - x ∣ < δ$ , step 1.2 gives $∣ \frac{g (y, t) - g (x, t)}{y - x} - h (x, t) ∣ < ε / (d - c)$ for every $t$ .

step 1.2step 2.1

4.1

The difference-quotient slice is continuous in $t$ and hence integrable. Linearity and [L4] now give $∣ \frac{G (y) - G (x)}{y - x} - \int_{c}^{d} h (x, t) d t ∣ < ε$ .

step 1.1step 3.1L4

5.1

Step 4.1 is precisely the relative derivative condition [L5]. It works with $y > x$ at $a$ , with $y < x$ at $b$ , and with both signs in the interior, proving the formula everywhere.

step 4.1L5∎

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-08-13Open item page →

The two FTC forms for a Riemann–Stieltjes integral with a $C^{1}$ integrator

Statement

Let $a < b$ . Suppose $α : [a, b] \to R$ is continuous, differentiable on $(a, b)$ , and its derivative extends to a continuous function $q : [a, b] \to R$ .

If $f : [a, b] \to R$ is Riemann integrable and continuous at $c$ , then $A (x) : = \int_{a}^{x} f d α$ is differentiable at $c$ and $A^{'} (c) = f (c) q (c)$ .
If $f$ is Riemann integrable, $G : [a, b] \to R$ is continuous and differentiable on $(a, b)$ , and $G^{'} (x) = f (x) q (x)$ there, then $\int_{a}^{b} f d α = G (b) - G (a)$ .

Endpoint derivatives in clause 1 are relative. Clause 2 does not divide by $q$ and remains valid where $q$ vanishes.

Facts & Assumptions

Given: The functions in the statement.

[L1]

For a continuous integrator whose interior derivative extends continuously as $q$ , every Riemann-integrable $f$ is Riemann--Stieltjes integrable and $\int_{u}^{v} f d α = \int_{u}^{v} f q$ on each closed subinterval (A continuously differentiable integrator reduces Stieltjes integration to ordinary integration).

[L2]

A continuous function on a compact interval is Riemann integrable, and products of Riemann-integrable functions are integrable; hence $f q$ is integrable because $q$ is continuous (A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion, If $f, g$ are integrable on $[a, b]$ then so are $∣ f ∣$ , $f^{2}$ , $f g$ , $\max (f, g)$ and $\min (f, g)$ , and $∣ \int_{a}^{b} f ∣ \leq \int_{a}^{b} ∣ f ∣$ ).

[L3]

The integral function of an integrable function is differentiable at each continuity point, with derivative equal to the integrand (The first fundamental theorem: if $f$ is integrable on $[a, b]$ and continuous at $c$ , then $F^{'} (c) = f (c)$ ; in particular a continuous $f$ has $F$ as a primitive).

[L4]

Proof

technique · reduction

1.1

By [L1], $A (x) = \int_{a}^{x} f (t) q (t) d t$ . The product $f q$ is integrable by [L2] and is continuous at $c$ .

givenL1L2

1.2

Under the hypotheses of clause 2, [L1] and [L2] give $\int_{a}^{b} f d α = \int_{a}^{b} f q$ , while $f q$ is an integrable extension of the interior derivative of $G$ .

givenL1L2

2.1

Applying [L3] to the ordinary integral function in step 1.1 gives $A^{'} (c) = f (c) q (c)$ , including either relative endpoint case.

step 1.1L3

3.1

Applying [L4] to $G$ gives $\int_{a}^{b} f q = G (b) - G (a)$ , and step 1.2 proves the second clause without any division by $q$ .

step 1.2L4∎

5 · Examples, counterexamples and false statements

None yet.

Sources

Standard references

Recommended treatments; not extraction sources.

The Fundamental Theorems of Calculus

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

Roadmap through the three strengths of FTC I and the five Riemann strengths of FTC II

Remark

Assuming Countable Choice, the integral function of a Riemann-integrable function is Lipschitz and differentiable almost everywhere, with derivative equal to the integrand there

Statement

Facts & Assumptions

Proof

Newton–Leibniz needs only continuity on [a,b][a,b], differentiability on (a,b)(a,b), and a Riemann-integrable extension of the interior derivative

Statement

Facts & Assumptions

Proof

Newton–Leibniz remains valid across finitely many exceptional interior points when the primitive is continuous

Statement

Facts & Assumptions

Proof

Botsko's theorem: if FF is continuous on [a,b][a,b], F′(x)=f(x)F′(x)=f(x) off a countable subset of (a,b)(a,b), and ff is Riemann integrable, then ∫abf=F(b)−F(a)∫ab​f=F(b)−F(a)

Statement

Facts & Assumptions

Proof

Integration by parts for continuous factors with Riemann-integrable extensions of their interior derivatives

Statement

Facts & Assumptions

Proof

Substitution for a continuous inner map with a Riemann-integrable extension of its interior derivative, without monotonicity or injectivity

Statement

Facts & Assumptions

Proof

For an integrable ff, the one-sided derivatives of F(x)=∫axfF(x)=∫ax​f equal the corresponding one-sided limits of ff; at a jump they are unequal

Statement

Facts & Assumptions

Proof

Leibniz's rule on a compact rectangle: an interior parameter derivative with a continuous extension may be passed through a Riemann integral

Statement

Facts & Assumptions

Proof

The two FTC forms for a Riemann–Stieltjes integral with a C1C1 integrator

Statement

Facts & Assumptions

Proof

5 · Examples, counterexamples and false statements

Sources

Standard references

Newton–Leibniz needs only continuity on $[a, b]$ , differentiability on $(a, b)$ , and a Riemann-integrable extension of the interior derivative

Botsko's theorem: if $F$ is continuous on $[a, b]$ , $F^{'} (x) = f (x)$ off a countable subset of $(a, b)$ , and $f$ is Riemann integrable, then $\int_{a}^{b} f = F (b) - F (a)$

For an integrable $f$ , the one-sided derivatives of $F (x) = \int_{a}^{x} f$ equal the corresponding one-sided limits of $f$ ; at a jump they are unequal

The two FTC forms for a Riemann–Stieltjes integral with a $C^{1}$ integrator