TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passverified 2026-08-10 (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.

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

Statement

Let $a < b$ be reals, let $G : [a, b] \to R$ be differentiable at every point of $[a, b]$ as a function on $[a, b]$ (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; at $a$ and $b$ this is the one-sided derivative), let $f : = G^{'}$ , and suppose $f$ is integrable on $[a, b]$ (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$ ). Then

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

Both hypotheses are needed and neither is removable. A function may be differentiable everywhere with $G^{'}$ not integrable — then the left-hand side does not exist (an everywhere differentiable function with unbounded derivative) — and an integrable $f$ need not be the derivative of anything (the sign function); both witnesses are on the companion page.

No continuity of $f$ is assumed, which is what makes this the working form: the theorem evaluates $\int_{a}^{b} f$ for every integrable derivative, not only for continuous integrands.

Facts & Assumptions

Given: Reals $a < b$ , a function $G : [a, b] \to R$ differentiable at every point of $[a, b]$ , $f : = G^{'}$ integrable on $[a, b]$ , and a partition $P = (n, t)$ of $[a, b]$ .

[L1]

For a partition $P = (n, t)$ of $[a, b]$ : $t_{0} = a$ , $t_{n} = b$ , $t_{i} < t_{i + 1}$ for $i < n$ , $Δ_{i} = t_{i + 1} - t_{i} > 0$ , and $I_{i} = [t_{i}, t_{i + 1}] \subseteq [a, b]$ (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, Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length).

[L2]

$L (f, P) = \sum_{i < n} m_{i} Δ_{i}$ and $U (f, P) = \sum_{i < n} M_{i} Δ_{i}$ with $m_{i} = \inf f [I_{i}]$ and $M_{i} = \sup f [I_{i}]$ , so $m_{i} \leq f (ξ) \leq M_{i}$ for every $ξ \in I_{i}$ (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}$ , Lower bound, bounded below, bounded set).

[L3]

$\underline{\int_{a}^{b}} f = \sup_{P} L (f, P)$ and $\overline{\int_{a}^{b}} f = \inf_{P} U (f, P)$ , and $f$ integrable means the two agree, their common value being $\int_{a}^{b} f$ (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$ ).

[L4]

Mean value theorem: if $u$ is continuous on $[p, q]$ with $p < q$ and differentiable at every point of $(p, q)$ , there is $ξ \in (p, q)$ with $u (q) - u (p) = u^{'} (ξ) (q - p)$ (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)$ ).

[L5]

A function differentiable at a point is continuous there, and the restriction of a differentiable function to a subinterval is differentiable with the same derivative at every point of that subinterval which is a limit point of it (A function differentiable at $c$ is continuous at $c$ , 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, 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).

[L6]

Finite sums: telescoping $\sum_{i < n} (c_{i + 1} - c_{i}) = c_{n} - c_{0}$ , and monotonicity in the terms (Finite sums and finite products, by recursion, Laws of finite sums and finite products, clauses 4 and 5).

[L7]

Ordered-field arithmetic: multiplying an inequality by a positive real preserves it, the order is total and transitive, and a number that is an upper bound of a set and also a lower bound of another set lies between their supremum and infimum (Ordered field, Complete ordered field (least-upper-bound property)).

Proof

technique · direct

1.1

Let $P = (n, t)$ be an arbitrary partition of $[a, b]$ and let $i < n$ . The restriction of $G$ to $I_{i} = [t_{i}, t_{i + 1}]$ is continuous on $I_{i}$ and differentiable at every point of $(t_{i}, t_{i + 1})$ , with the same derivative $f$ there, by [L5] and [L1].

givenL1L5

2.1

By [L4] applied on $I_{i}$ there is $ξ_{i} \in (t_{i}, t_{i + 1})$ with $G (t_{i + 1}) - G (t_{i}) = f (ξ_{i}) Δ_{i}$ ; since $ξ_{i} \in I_{i}$ and $Δ_{i} > 0$ , [L2] gives $m_{i} Δ_{i} \leq G (t_{i + 1}) - G (t_{i}) \leq M_{i} Δ_{i}$ .

step 1.1L1L2L4L7

3.1

Step 2.1 holds for every $i < n$ , so monotonicity of finite sums applies to the three families and gives $\sum_{i < n} m_{i} Δ_{i} \leq \sum_{i < n} (G (t_{i + 1}) - G (t_{i})) \leq \sum_{i < n} M_{i} Δ_{i}$ .

step 2.1L6

4.1

The middle sum telescopes to $G (t_{n}) - G (t_{0}) = G (b) - G (a)$ by [L6] and [L1], so $L (f, P) \leq G (b) - G (a) \leq U (f, P)$ by [L2].

step 3.1L1L2L6

5.1

Step 4.1 holds for every partition $P$ , so $G (b) - G (a)$ is an upper bound of the set of lower sums and a lower bound of the set of upper sums; hence $\underline{\int_{a}^{b}} f \leq G (b) - G (a) \leq \overline{\int_{a}^{b}} f$ by [L3] and [L7].

step 4.1L3L7

6.1

Since $f$ is integrable the two integrals coincide with $\int_{a}^{b} f$ , so $\int_{a}^{b} f = G (b) - G (a)$ .

step 5.1L3∎

Remarks

No choice principle is spent, and no sequence of tags is ever formed. The usual proof selects one $ξ_{i}$ per subinterval and assembles the Riemann sum $\sum_{i} f (ξ_{i}) Δ_{i}$ , which is a choice from finitely many nonempty sets. The proof above never forms that family: step 2.1 proves, for an arbitrary fixed $i$ , the inequality $m_{i} Δ_{i} \leq G (t_{i + 1}) - G (t_{i}) \leq M_{i} Δ_{i}$ , which is a universally quantified statement about $i$ and needs no selection, and step 3.1 then sums the inequality. The telescoping identity supplies the middle term without any tags at all.
The hypothesis is differentiability at every point of the closed interval. It is not enough to be differentiable on $(a, b)$ and continuous on $[a, b]$ in the argument as written, because step 2.1 uses the derivative only on open subintervals but the definition $f = G^{'}$ has to name a function on all of $[a, b]$ for $\int_{a}^{b} f$ to mean anything. Changing $f$ at the two endpoints changes neither its integrability nor its integral (Changing an integrable function at finitely many points changes neither its integrability nor its integral), so the reader who prefers the weaker hypothesis loses nothing.
This is the half of the fundamental theorem that computes. The other half, 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, produces a primitive; this one evaluates an integral once a primitive is known, and it is the tool the companion page reaches for whenever a primitive is available. Where no primitive is at hand the companion page computes instead by splitting at a jump and using the integral of a constant; no claim is made here about how many of its computations take which route.
Forward references, orientation only. The two witnesses showing neither hypothesis is removable are A function differentiable on $[0, 1]$ whose derivative is unbounded, hence not Riemann integrable ↗ and The sign function is Riemann integrable on $[- 1, 1]$ and has no primitive there ↗ on the companion page; nothing above depends on either.

Depends on

Used by

…and 47 more results.

Dependency tree · two levels

49 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

Fundamental theorem of calculus (Wikipedia) (standard reference, not scraped)
W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 6 (standard reference, not scraped)
Carnegie Mellon 21-269, Riemann integration notes (standard reference, not scraped)
J. Lebl, Basic Analysis I, Fundamental theorem of calculus (standard reference, not scraped)

The second fundamental theorem: if GG is differentiable on [a,b][a,b] with G′=fG′=f and ff is integrable, then ∫abf=G(b)−G(a)∫ab​f=G(b)−G(a)