TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-13

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.

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∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 66 results over 17 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

J. K. Hunter, An Introduction to Real Analysis, Chapter 12 (standard reference, not scraped)
J. Lebl, Basic Analysis I & II, Section 5.3 (standard reference, not scraped)

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