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.

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

Properties of the Integral and the Working FTC

1 · Prerequisites

2 · Summary

Objective. The previous page defined the integral and settled which functions have one. This page makes it usable: the algebra of the integral, its behaviour under splitting the interval, and the two fundamental theorems in the form that computes. It ends with three theorems that are applications of the machinery rather than parts of it: Bonnet's second mean value theorem, the vanishing of a nonnegative continuous integrand with zero integral, and the integral test for series.

A convention has to be minted first, and it is not decoration. 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$ is stated under the standing hypothesis $a < b$ of 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, so $\int_{a}^{b} f$ is an undefined symbol whenever $a \geq b$ . The integral with oriented limits: $\int_{a}^{a} f : = 0$ and $\int_{b}^{a} f : = - \int_{a}^{b} f$ extends the notation by $\int_{a}^{a} f : = 0$ and $\int_{b}^{a} f : = - \int_{a}^{b} f$ ; nothing new is integrated, and the three clauses sit on the three cases of trichotomy so no consistency check arises. Without it the additivity identity, the integral function and the substitution theorem could not be stated in the generality they are proved in. Conventions of this page, and which sharpenings of the integral are taken up later in the reading order records the convention, the one inequality on this page that is not orientation-invariant, and what the page costs in choice.

The algebra. A function integrable on $[a, b]$ is integrable on every closed subinterval restricts an integrable function to a closed subinterval, re-indexing the partition explicitly rather than saying "restrict". 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$ proves closure under sums and scalar multiples; the two halves are genuinely different, because $\sup (f + g) \leq \sup f + \sup g$ can be strict — so the sum case squeezes rather than computes — while a negative scalar exchanges the roles of $\sup$ and $\inf$ . If $f \leq g$ on $[a, b]$ and both are integrable then $\int_{a}^{b} f \leq \int_{a}^{b} g$ ; and $m (b - a) \leq \int_{a}^{b} f \leq M (b - a)$ is short, and it is what every later estimate of an integral against a pointwise bound goes through; seven of the sixteen later items on this page cite it. 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$ proves the splitting in both directions and then the oriented identity $\int_{u}^{v} f + \int_{v}^{w} f = \int_{u}^{w} f$ for arbitrary $u, v, w$ ; that last clause is proved by observing that the oriented integral is a difference of values of one function of one variable, not by listing six orderings. Changing an integrable function at finitely many points changes neither its integrability nor its integral shows the integral cannot see a finite set, the one delicate point being that a partition point lies in two subintervals.

Composition, and the order of the hypotheses. If $f$ is integrable on $[a, b]$ with values in $[m, M]$ and $φ$ is continuous on $[m, M]$ , then $φ \circ f$ is integrable is the one place where the classical argument does not transfer: if $f$ is integrable with values in $[m, M]$ and $φ$ is continuous on $[m, M]$ , then $φ \circ f$ is integrable. The classical proof splits the index range into good and bad indices; the finite-sum laws available here are stated for $\sum_{i < n}$ and none of them splits a range into a subset and its complement, so the split is carried instead by one inequality valid at every index. The order matters: continuous after integrable is the hypothesis, and the reversal is refuted on the companion page. 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 ∣$ reads off $∣ f ∣$ , $f^{2}$ , $f g$ , $\max (f, g)$ , $\min (f, g)$ and the triangle inequality for the integral, using the polarisation identity to reduce a two-variable operation to the one-variable theorem.

The integral function and the two fundamental theorems. The integral function $F (x) : = \int_{a}^{x} f$ of an integrable $f$ introduces $F (x) = \int_{a}^{x} f$ and discharges its own well-definedness. The integral function of a bounded integrable $f$ is Lipschitz, hence uniformly continuous shows $F$ is Lipschitz for every integrable $f$ , with no continuity assumed, which is what makes the hypotheses of the next theorem visible as hypotheses. 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 proves $F^{'} (c) = f (c)$ at each point of continuity of $f$ , from the definition of the derivative and not from a mean value theorem, with the estimate written out on both sides of $c$ because the factor $1 / (x - c)$ changes sign. 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)$ is the working half: if $G$ is differentiable on $[a, b]$ with $G^{'} = f$ integrable, then $\int_{a}^{b} f = G (b) - G (a)$ , and no continuity of $f$ is needed. Its proof selects no mean-value points and spends no choice. Every continuous function on an interval has a primitive; two primitives differ by a constant; and $\int_{a}^{b} f = G (b) - G (a)$ for any primitive $G$ assembles the two and 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 into existence, uniqueness up to a constant, and evaluation.

The two computational rules. If $u, v$ are differentiable on $[a, b]$ with $u^{'}, v^{'}$ integrable, then $\int_{a}^{b} u v^{'} = u (b) v (b) - u (a) v (a) - \int_{a}^{b} u^{'} v$ and Substitution: if $φ$ is differentiable on $[c, d]$ with $φ^{'}$ integrable and $f$ is continuous on an interval containing $φ ([c, d])$ , then $\int_{φ (c)}^{φ (d)} f = \int_{c}^{d} (f \circ φ) φ^{'}$ follow from the second fundamental theorem applied to $u v$ and to $F \circ φ$ . Both check integrability of the products explicitly — that is the step usually skipped, and it is why the hypotheses are what they are. Substitution assumes neither injectivity nor monotonicity of $φ$ , which is exactly why its limits are written with the orientation convention.

Three applications. Bonnet's second mean value theorem: for $f$ monotone and $g$ integrable on $[a, b]$ there is $ξ \in [a, b]$ with $\int_{a}^{b} f g = f (a) \int_{a}^{ξ} g + f (b) \int_{ξ}^{b} g$ proves Bonnet's theorem in the general monotone form: $f$ monotone and $g$ integrable, with no differentiability and no continuity of $f$ . The route is Abel summation by parts (Abel summation by parts: with $A_{n} = \sum_{k < n} a_{k}$ one has $\sum_{k < n} a_{k} b_{k} = A_{n} b_{n - 1} - \sum_{k < n - 1} A_{k + 1} (b_{k + 1} - b_{k})$ for every $n \geq 1$ ) on the values of the integral function at the partition points, followed by an estimate that is driven to zero by the integrability of $f$ alone; no tagged partition and no mesh condition appears. A continuous $f \geq 0$ on $[a, b]$ with $\int_{a}^{b} f = 0$ is identically $0$ is the exact repair of a published false statement, now provable because additivity is available. The integral test: for $f \geq 0$ nonincreasing on $[0, \infty)$ , $\sum_{k} f (k)$ converges if and only if the sequence $(\int_{0}^{N} f)_{N}$ is bounded, with $\int_{0}^{N} f \leq \sum_{k < N} f (k) \leq f (0) + \int_{0}^{N} f$ is stated with proper integrals only: its conclusion is that the sequence $(\int_{0}^{N} f)_{N}$ is bounded, not that an improper integral converges, because improper integrals are not defined at this point in the reading order — and both its sum and its integral begin at $0$ , since $N$ contains $0$ .

What is deliberately absent. Taylor's integral remainder needs higher derivatives and is not developed on this page. The current Darboux/L'Hopital/Taylor page also explicitly excludes the integral remainder. Bounded variation with the Riemann-Stieltjes integral, and improper integrals, are each a later page of this track; the sharp form of the fundamental theorem is not a planned page at all but a recorded-not-proved result, The sharp fundamental theorem of calculus (absolute continuity) ‡. Arzelà's bounded convergence theorem is not here: it is a genuine theorem about the Riemann integral, but no complete proof route was certifiable at scaffold time, and the counterexample that motivates it — Continuous $f_{n} \to 0$ pointwise on $[0, 1]$ with $\int_{0}^{1} f_{n} = 1$ for every $n$ on the companion page — stands on its own without asserting anything about the bounded case. Conventions of this page, and which sharpenings of the integral are taken up later in the reading order lists all of this as reading order and makes no claim about what the library proves.

Twenty items, of which two are definitions, one is the page ledger, and the rest are the lemmas, theorems and corollaries above. The companion page works thirteen examples, counterexamples and false statements against them.

3 · Logical flowchart

4 · Definitions, theorems and proofs

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (z-ai/glm-5.2)audited 2026-07-29Open item page →

The integral with oriented limits: $\int_{a}^{a} f : = 0$ and $\int_{b}^{a} f : = - \int_{a}^{b} f$

Definition

Why this item is first. The published definition of the integral does not cover this page. 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$ is stated for reals $a < b$ , because the partitions it quantifies over are those of 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, whose standing hypothesis is $a < b$ : with $a = b$ the chain $a = t_{0} < \dots < t_{n} = b$ is unsatisfiable. So $\int_{a}^{b} f$ is an undefined symbol whenever $a \geq b$ , and every additivity statement below would be ill-formed as it is usually written. This item extends the notation, and nothing else: the object it names is still the Darboux integral of 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$ .

Let $u, v \in R$ and write

$[u \land v, u \lor v] : = the closed interval with endpoints u and v$

(Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length). Let $f$ be a real-valued function whose domain contains that interval. Say that $f$ is integrable between $u$ and $v$ when either $u = v$ , or $u \neq v$ and the restriction of $f$ to $[u \land v, u \lor v]$ is bounded (Lower bound, bounded below, bounded set) and Darboux integrable there (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$ , 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}$ ). For such $f$ define

$\int_{u}^{v} f : = {\begin{cases} the Darboux integral of f over [u, v] & if u < v, \\ 0 & if u = v, \\ - \int_{v}^{u} f & if u > v . \end{cases}$

There is nothing to check for consistency. The three clauses are indexed by the three cases of trichotomy, $u < v$ , $u = v$ and $u > v$ , which are mutually exclusive and exhaustive; no pair of them ever applies to the same $(u, v)$ . In particular the first clause is untouched, so on $u < v$ this is the published integral verbatim and every published theorem about it applies unchanged.

The middle clause is a stipulation, not a computation. It is not claimed that $0$ is a value forced by the $u < v$ definition in any limiting sense; that definition simply says nothing at $u = v$ , and $\int_{u}^{u} f : = 0$ is what is written there. It is also unconditional: no hypothesis on $f$ beyond being defined at $u$ is asked for, since the case $u = v$ never refers to a partition.

The two consequences used throughout the page

Antisymmetry, for every pair. For all reals $u, v$ with $f$ integrable between them,

$\int_{u}^{v} f = - \int_{v}^{u} f .$

Indeed if $u < v$ then $v > u$ and the third clause reads $\int_{v}^{u} f = - \int_{u}^{v} f$ , which rearranges to the display; if $u = v$ both sides are $0$ ; and if $u > v$ the third clause is the display itself.

Absolute values agree. Consequently $∣ \int_{u}^{v} f ∣ = ∣ \int_{v}^{u} f ∣$ for every such pair.

An obligation recorded here and discharged elsewhere. With this convention the additivity identity

$\int_{u}^{v} f + \int_{v}^{w} f = \int_{u}^{w} f$

holds for every arrangement of $u, v, w$ in an interval on which $f$ is integrable, not only for $u < v < w$ . That is a theorem and not part of this definition; it is proved as the last clause of 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$ , and nothing on this page uses it before it is proved there.

Remarks

This is notation, and it is a real notation. Without it the substitution theorem could not be stated with the limits $φ (c)$ and $φ (d)$ in the order the map produces them, since a differentiable $φ$ need be neither injective nor monotone; and the integral function $x \mapsto \int_{a}^{x} f$ would be undefined at $x = a$ .
One published inequality is not orientation-invariant, and that is a trap. The estimate $∣ \int_{u}^{v} f ∣ \leq \int_{u}^{v} ∣ f ∣$ is guaranteed only for $u \leq v$ : at $u > v$ the right-hand side is $- \int_{v}^{u} ∣ f ∣ \leq 0$ while the left-hand side is $\geq 0$ , so the inequality fails whenever $\int_{v}^{u} ∣ f ∣ > 0$ . The form valid for every pair is $∣ \int_{u}^{v} f ∣ \leq ∣ \int_{u}^{v} ∣ f ∣ ∣$ , and this is stated where it is proved (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 ∣$ ).
Integrability is a property of the unordered pair. By construction, $f$ is integrable between $u$ and $v$ if and only if it is integrable between $v$ and $u$ , since both refer to the same closed interval; only the sign of the value remembers the order.

LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-29Open item page →

A function integrable on $[a, b]$ is integrable on every closed subinterval

Statement

$a \leq c < d \leq b .$

Then the restriction of $f$ to $[c, d]$ is bounded (Lower bound, bounded below, bounded set) and integrable on $[c, d]$ .

The degenerate case $c = d$ is not an omission: there $\int_{c}^{c} f = 0$ by The integral with oriented limits: $\int_{a}^{a} f : = 0$ and $\int_{b}^{a} f : = - \int_{a}^{b} f$ , and no partition of $[c, d]$ exists to speak of (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).

Facts & Assumptions

Given: Reals $a < b$ , an integrable $f : [a, b] \to R$ , and reals $c, d$ with $a \leq c < d \leq b$ . Write $g$ for the restriction of $f$ to $[c, d]$ .

[L1]

Riemann's criterion: a bounded function on a closed bounded interval with distinct endpoints is integrable if and only if for every real $ε > 0$ there is a partition $P$ of that interval with $U (\cdot, P) - L (\cdot, P) < ε$ (Riemann's criterion: a bounded $f$ on $[a, b]$ is Darboux integrable if and only if for every real $ε > 0$ there is a partition $P$ with $U (f, P) - L (f, P) < ε$ , 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$ ).

[L2]

For a partition $P$ of $[a, b]$ and a point $p \in [a, b]$ , the partition $P + p$ satisfies $pts (P + p) = pts (P) \cup {p}$ and refines $P$ ; a refinement of a refinement refines the original, since the point-set inclusions compose (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).

[L3]

If $P^{'}$ refines $P$ then $L (f, P) \leq L (f, P^{'}) \leq U (f, P^{'}) \leq U (f, P)$ (Refining a partition raises the lower Darboux sum and lowers the upper one, and every lower sum is at most every upper sum: $L (f, P) \leq L (f, P^{'}) \leq U (f, P^{'}) \leq U (f, P)$ when $P^{'}$ refines $P$ , and $L (f, P) \leq U (f, Q)$ for arbitrary partitions $P$ and $Q$ ; moreover the two changes are at most $2 M (n^{'} - n) ∥ P ∥$ , claim 1).

[L4]

For a partition $R = (n, t)$ of an interval and bounded $h$ on it: $L (h, R) = \sum_{i < n} m_{i} Δ_{i}$ , $U (h, R) = \sum_{i < n} M_{i} Δ_{i}$ with $m_{i} = \inf h [I_{i}]$ , $M_{i} = \sup h [I_{i}]$ , $I_{i} = [t_{i}, t_{i + 1}]$ , $Δ_{i} = t_{i + 1} - t_{i} > 0$ , and $M_{i} - m_{i} \geq 0$ (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}$ , 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).

[L5]

Finite sums: additivity, scaling, splitting at an intermediate index with $\sum_{k = m}^{n - 1} a_{k} = \sum_{j < n - m} a_{m + j}$ , and monotonicity in the terms, so that a sum of nonnegative terms is at most a sum containing those terms among others (Finite sums and finite products, by recursion, Laws of finite sums and finite products, clauses 1 to 4).

[L6]

A partition $P^{'} = (n^{'}, t^{'})$ of $[a, b]$ has $t^{'}$ strictly increasing on indices $\leq n^{'}$ , hence injective there, so a point of $pts (P^{'})$ is $t_{j}^{'}$ for exactly one $j \leq n^{'}$ ; and $j < k$ gives $t_{j}^{'} < t_{k}^{'}$ (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).

[L7]

A restriction of a bounded function is bounded: the same $M$ serves fewer points (Lower bound, bounded below, bounded set).

Proof

technique · direct

1.1

$g$ is bounded on $[c, d]$ , since $[c, d] \subseteq [a, b]$ and $f$ is bounded on $[a, b]$ , integrability presupposing boundedness.

givenL7

1.2

Let a real $ε > 0$ be given, and fix a partition $P$ of $[a, b]$ with $U (f, P) - L (f, P) < ε$ .

givenL1choose

2.1

Put $P^{'} : = (P + c) + d$ , a partition of $[a, b]$ refining $P$ whose point set contains $c$ and $d$ .

step 1.2L2construct

3.1

By [L3] applied to the pair $(P, P^{'})$ , $U (f, P^{'}) - L (f, P^{'}) \leq U (f, P) - L (f, P) < ε$ .

step 1.2step 2.1L3

3.2

Write $P^{'} = (n^{'}, t^{'})$ and fix the unique indices $p, q \leq n^{'}$ with $t_{p}^{'} = c$ and $t_{q}^{'} = d$ ; then $p < q$ , because $c < d$ and $t^{'}$ is increasing on those indices.

step 2.1L6choose

4.1

Define $Q : = (q - p, s)$ by $s_{i} : = t_{p + i}^{'}$ for $i \leq q - p$ and $s_{k} : = d$ for $k \geq q - p$ . Then $s_{0} = t_{p}^{'} = c$ , $s_{q - p} = t_{q}^{'} = d$ , and $s_{i} < s_{i + 1}$ for $i < q - p$ by [L6], with $q - p \geq 1$ ; so $Q$ is a partition of $[c, d]$ , its $i$ -th subinterval is $[t_{p + i}^{'}, t_{p + i + 1}^{'}] = I_{p + i}^{'}$ and its $i$ -th length is $Δ_{p + i}^{'}$ .

step 3.2L6construct

5.1

For $i < q - p$ the $i$ -th subinterval of $Q$ is $I_{p + i}^{'} \subseteq [c, d]$ , and $g$ agrees with $f$ there, so the extreme values of $g$ on it are $M_{p + i}^{'}$ and $m_{p + i}^{'}$ ; hence $U (g, Q) - L (g, Q) = \sum_{i < q - p} (M_{p + i}^{'} - m_{p + i}^{'}) Δ_{p + i}^{'}$ by [L4] and [L5].

step 4.1L4L5

6.1

Every term $(M_{j}^{'} - m_{j}^{'}) Δ_{j}^{'}$ is nonnegative by [L4], and splitting $\sum_{j < n^{'}}$ first at $p$ and then at $q$ exhibits $\sum_{i < q - p} (M_{p + i}^{'} - m_{p + i}^{'}) Δ_{p + i}^{'}$ as one of the three pieces of $\sum_{j < n^{'}} (M_{j}^{'} - m_{j}^{'}) Δ_{j}^{'}$ , the other two being nonnegative; so the displayed sum is at most $U (f, P^{'}) - L (f, P^{'})$ .

step 5.1L4L5

7.1

Combining, $U (g, Q) - L (g, Q) \leq U (f, P^{'}) - L (f, P^{'}) < ε$ .

step 3.1step 5.1step 6.1

8.1

Since $ε > 0$ was arbitrary and $g$ is bounded, [L1] applies on $[c, d]$ and $g$ is integrable there.

step 1.1step 1.2step 7.1L1∎

Remarks

The one step that is not bookkeeping is the re-indexing. A partition in this library is a pair $(n, t)$ with a tail convention (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), not a set of points, so "restrict $P^{'}$ to $[c, d]$ " is not a defined operation; step 4.1 writes the restricted list out, shifts its index by $p$ and resets its tail to $d$ . Everything else follows from the fact that dropping nonnegative terms from a finite sum cannot increase it.
The converse is also true, and is proved separately. Integrability on $[a, c]$ and on $[c, b]$ gives integrability on $[a, b]$ ; that direction needs a splice rather than a restriction and is the second half of 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$ .

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passverified 2026-08-10 (gpt-5.6-terra-codex-subscription)Open item page →

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$

Statement

Let $a < b$ be reals and let $f, g : [a, b] \to R$ be integrable (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:

$f + g$ is integrable on $[a, b]$ and $\int_{a}^{b} (f + g) = \int_{a}^{b} f + \int_{a}^{b} g$ ;
for every real $λ$ , $λ f$ is integrable on $[a, b]$ and $\int_{a}^{b} λ f = λ \int_{a}^{b} f$ ;
consequently, for all reals $λ, μ$ the function $λ f + μ g$ is integrable and $\int_{a}^{b} (λ f + μ g) = λ \int_{a}^{b} f + μ \int_{a}^{b} g;$
the same identity holds with oriented limits: if $u, v \in [a, b]$ and $f, g$ are integrable between $u$ and $v$ (The integral with oriented limits: $\int_{a}^{a} f : = 0$ and $\int_{b}^{a} f : = - \int_{a}^{b} f$ ), then $\int_{u}^{v} (λ f + μ g) = λ \int_{u}^{v} f + μ \int_{u}^{v} g$ .

Linearity of the integral is not linearity of the Darboux sums, and the proof of claim 1 has to squeeze rather than compute. On a subinterval the inequality $\sup (f + g) \leq \sup f + \sup g$ can be strict — take $f (x) = x$ and $g (x) = - x$ on $[0, 1]$ , where the left side is $0$ and the right side is $1$ — so $U (f + g, P)$ is in general strictly below $U (f, P) + U (g, P)$ and no identity between upper sums is available. Claim 2, by contrast, is an identity at the level of the sums, with the roles of $\sup$ and $\inf$ exchanged when $λ < 0$ .

Facts & Assumptions

Given: Reals $a < b$ , integrable $f, g : [a, b] \to R$ , reals $λ, μ$ , and a real $ε > 0$ .

[L1]

Riemann's criterion: a bounded $h$ on $[a, b]$ is integrable if and only if for every real $η > 0$ there is a partition $P$ with $U (h, P) - L (h, P) < η$ (Riemann's criterion: a bounded $f$ on $[a, b]$ is Darboux integrable if and only if for every real $ε > 0$ there is a partition $P$ with $U (f, P) - L (f, P) < ε$ ).

[L2]

For every partition $P$ and bounded $h$ : $L (h, P) \leq \underline{\int_{a}^{b}} h \leq \overline{\int_{a}^{b}} h \leq U (h, P)$ , and $h$ is integrable exactly when the two integrals agree, their common value being $\int_{a}^{b} h$ ; the lower integral is $\sup_{P} L (h, P)$ and the upper is $\inf_{P} U (h, P)$ (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$ , Suprema and infima are unique).

[L3]

$L (h, P) = \sum_{i < n} m_{i} (h) Δ_{i}$ and $U (h, P) = \sum_{i < n} M_{i} (h) Δ_{i}$ , where $m_{i} (h) = \inf h [I_{i}]$ and $M_{i} (h) = \sup h [I_{i}]$ over the subintervals $I_{i}$ of $P = (n, t)$ , with $Δ_{i} > 0$ ; an integrable function is bounded, and a sum of two bounded functions and a scalar multiple of a bounded function are bounded (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}$ , 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, Lower bound, bounded below, bounded set).

[L4]

If $P^{'}$ refines $P$ then $L (h, P) \leq L (h, P^{'}) \leq U (h, P^{'}) \leq U (h, P)$ ; the common refinement $P_{1} \lor P_{2}$ refines both (Refining a partition raises the lower Darboux sum and lowers the upper one, and every lower sum is at most every upper sum: $L (f, P) \leq L (f, P^{'}) \leq U (f, P^{'}) \leq U (f, P)$ when $P^{'}$ refines $P$ , and $L (f, P) \leq U (f, Q)$ for arbitrary partitions $P$ and $Q$ ; moreover the two changes are at most $2 M (n^{'} - n) ∥ P ∥$ , 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).

[L5]

Finite sums are additive and homogeneous: $\sum_{i < n} (x_{i} + y_{i}) = \sum_{i < n} x_{i} + \sum_{i < n} y_{i}$ and $\sum_{i < n} λ x_{i} = λ \sum_{i < n} x_{i}$ (Finite sums and finite products, by recursion, Laws of finite sums and finite products, clauses 1 and 2).

[L6]

A supremum is the least upper bound and an infimum the greatest lower bound; both exist for a nonempty bounded set and are unique (Complete ordered field (least-upper-bound property), Greatest lower bound (infimum), Suprema and infima are unique).

[L7]

Reflection: writing $- S = {- s : s \in S}$ , a real $u$ is an upper bound of $S$ exactly when $- u$ is a lower bound of $- S$ , and conversely; hence $\sup (- S) = - \inf S$ and $\inf (- S) = - \sup S$ for nonempty bounded $S$ , by [L6] (Reflection through zero exchanges upper and lower bounds).

[L8]

The constant function $0$ is integrable with $\int_{a}^{b} 0 = 0$ (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)$ ).

[L9]

Ordered-field arithmetic: adding a constant and multiplying by a positive quantity preserve an inequality, the order is total and transitive, and a real $x$ with $∣ x ∣ < η$ for every real $η > 0$ is $0$ (Ordered field, Complete ordered field (least-upper-bound property)). These order facts are used in their nonstrict form as well, obtained by adjoining the case of equality.

[L10]

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

Proof

technique · direct

1.1

$f$ , $g$ , $f + g$ and $λ f$ are bounded on $[a, b]$ , so all their Darboux sums and integrals are defined.

givenL3

1.2

For every partition $P = (n, t)$ and every $i < n$ : $f (x) + g (x) \leq M_{i} (f) + M_{i} (g)$ for $x \in I_{i}$ , so $M_{i} (f) + M_{i} (g)$ is an upper bound of $(f + g) [I_{i}]$ and $M_{i} (f + g) \leq M_{i} (f) + M_{i} (g)$ by [L6]; dually $m_{i} (f + g) \geq m_{i} (f) + m_{i} (g)$ .

L3L6

1.3

Fix partitions $P_{1}$ and $P_{2}$ with $U (f, P_{1}) - L (f, P_{1}) < ε \cdot 2^{- 1}$ and $U (g, P_{2}) - L (g, P_{2}) < ε \cdot 2^{- 1}$ , and put $P : = P_{1} \lor P_{2}$ .

givenL1L4choose

1.4

Claim 2, the case $λ = 0$ . Then $λ f$ is the constant function $0$ , integrable with integral $0 = 0 \cdot \int_{a}^{b} f$ .

1.5

Claim 2, the case $λ > 0$ . For every partition $P$ and every $i < n$ , $λ M_{i} (f)$ is an upper bound of $(λ f) [I_{i}]$ , and any upper bound $w$ of $(λ f) [I_{i}]$ gives the upper bound $w / λ$ of $f [I_{i}]$ , whence $M_{i} (f) \leq w / λ$ and $λ M_{i} (f) \leq w$ ; so $M_{i} (λ f) = λ M_{i} (f)$ by [L6], and dually $m_{i} (λ f) = λ m_{i} (f)$ .

L3L6L9

1.6

Claim 2, the case $λ = - 1$ . For every $P$ and $i < n$ , $(- f) [I_{i}] = - (f [I_{i}])$ , so $M_{i} (- f) = - m_{i} (f)$ and $m_{i} (- f) = - M_{i} (f)$ by [L7].

L3L7

2.1

By [L4], $U (f, P) - L (f, P) < ε \cdot 2^{- 1}$ and $U (g, P) - L (g, P) < ε \cdot 2^{- 1}$ .

step 1.3L4

2.2

Summing the inequalities of step 1.2 over $i < n$ against the positive weights $Δ_{i}$ and using [L5] gives $L (f, P) + L (g, P) \leq L (f + g, P) \leq U (f + g, P) \leq U (f, P) + U (g, P)$ .

step 1.2L3L5L9

2.3

With step 1.5 and [L5], $U (λ f, P) = λ U (f, P)$ and $L (λ f, P) = λ L (f, P)$ for $λ > 0$ ; hence $U (λ f, P) - L (λ f, P) = λ (U (f, P) - L (f, P))$ , which [L1] makes smaller than any prescribed positive number by choosing $P$ suitably, so $λ f$ is integrable.

step 1.5L1L3L5L9

2.4

With step 1.6 and [L5], $U (- f, P) = - L (f, P)$ and $L (- f, P) = - U (f, P)$ , so $U (- f, P) - L (- f, P) = U (f, P) - L (f, P)$ and $- f$ is integrable by [L1]; and by [L7] applied to the sets of Darboux sums, $\overline{\int_{a}^{b}} (- f) = - \underline{\int_{a}^{b}} f$ and $\underline{\int_{a}^{b}} (- f) = - \overline{\int_{a}^{b}} f$ , so $\int_{a}^{b} (- f) = - \int_{a}^{b} f$ .

step 1.6L1L2L5L7

3.1

Hence $U (f + g, P) - L (f + g, P) \leq (U (f, P) - L (f, P)) + (U (g, P) - L (g, P)) < ε$ , so $f + g$ is integrable by [L1], $ε > 0$ having been arbitrary.

step 1.1step 2.1step 2.2L1L9

3.2

Moreover the set of lower sums of $λ f$ is $λ$ times the set of lower sums of $f$ , and a supremum scales by a positive factor, by the argument of step 1.5 applied to that set; so $\underline{\int_{a}^{b}} λ f = λ \underline{\int_{a}^{b}} f$ , and likewise for the upper integrals, giving $\int_{a}^{b} λ f = λ \int_{a}^{b} f$ .

step 1.5step 2.3L2L6L9

4.1

Both $\int_{a}^{b} (f + g)$ and $\int_{a}^{b} f + \int_{a}^{b} g$ lie in the interval from $L (f, P) + L (g, P)$ to $U (f, P) + U (g, P)$ : the first by [L2] and step 2.2, the second by [L2] applied to $f$ and to $g$ separately.

step 2.1step 2.2step 3.1L2

4.2

Claim 2 for $λ < 0$ . Then $- λ > 0$ and $λ f = (- λ) (- f)$ , so steps 2.3, 2.4 and 3.2 give integrability and the required identities and $\int_{a}^{b} λ f = (- λ) \int_{a}^{b} (- f) = (- λ) (- \int_{a}^{b} f) = λ \int_{a}^{b} f$ .

step 2.3step 3.2step 2.4L9

5.1

That interval has length less than $ε$ by step 2.1, so $∣ \int_{a}^{b} (f + g) - \int_{a}^{b} f - \int_{a}^{b} g ∣ < ε$ ; as $ε > 0$ was arbitrary the difference is $0$ , which is claim 1.

step 2.1step 4.1L9

5.2

Claim 2 is now proved in all three cases $λ = 0$ , $λ > 0$ and $λ < 0$ , which are exhaustive by trichotomy.

step 1.4step 2.3step 3.2step 4.2L9

6.1

Claim 3. By claim 2 the functions $λ f$ and $μ g$ are integrable with integrals $λ \int_{a}^{b} f$ and $μ \int_{a}^{b} g$ , and by claim 1 their sum is integrable with the sum of those integrals.

step 5.1step 5.2

7.1

Claim 4. If $u < v$ then $u, v \in [a, b]$ and claim 3 applies verbatim on $[u, v]$ ; if $u = v$ both sides are $0$ by [L10]; and if $u > v$ then applying the case $u < v$ to the pair $(v, u)$ and multiplying by $- 1$ gives the identity, by [L10].

step 6.1L10∎

Remarks

Why claim 1 cannot be an identity of Darboux sums. The example in the statement shows $\sup (f + g) < \sup f + \sup g$ is possible on a single subinterval, so $U (f + g, P) = U (f, P) + U (g, P)$ is false in general. What survives is the pair of inequalities of step 1.2, and they are enough because the gap between them is squeezed to $0$ by Riemann's criterion: a bounded $f$ on $[a, b]$ is Darboux integrable if and only if for every real $ε > 0$ there is a partition $P$ with $U (f, P) - L (f, P) < ε$ .
The two scalar cases really are different. For $λ > 0$ the extreme values scale; for $λ < 0$ they are exchanged, because multiplying by a negative reverses the order (Reflection through zero exchanges upper and lower bounds). Merging the cases and writing $U (λ f, P) = λ U (f, P)$ for all $λ$ would be false at $λ = - 1$ , where the correct identity is $U (- f, P) = - L (f, P)$ .
The set of integrable functions on $[a, b]$ is closed under the operations named here and under more. Products, absolute values and the lattice operations are also integrable, but none of them is obtained from linearity alone: the proofs of 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 ∣$ all pass through If $f$ is integrable on $[a, b]$ with values in $[m, M]$ and $φ$ is continuous on $[m, M]$ , then $φ \circ f$ is integrable, with linearity used only to recombine the pieces.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passverified 2026-08-10 (gpt-5.6-terra-codex-subscription)Open item page →

If $f \leq g$ on $[a, b]$ and both are integrable then $\int_{a}^{b} f \leq \int_{a}^{b} g$ ; and $m (b - a) \leq \int_{a}^{b} f \leq M (b - a)$

Statement

Nonnegativity. If $f (x) \geq 0$ for every $x \in [a, b]$ then $\int_{a}^{b} f \geq 0$ .
Monotonicity. If $f (x) \leq g (x)$ for every $x \in [a, b]$ then $\int_{a}^{b} f \leq \int_{a}^{b} g .$
Two-sided bound. If $m \leq f (x) \leq M$ for every $x \in [a, b]$ , with $m, M$ real, then $m (b - a) \leq \int_{a}^{b} f \leq M (b - a) .$

Equality in claim 1 does not force $f$ to vanish. A nonnegative integrable function with integral $0$ may be positive at infinitely many points; that is FALSE: a nonnegative Riemann integrable function on $[a, b]$ with $\int_{a}^{b} f = 0$ is identically zero on the previous page's companion. Under the additional hypothesis of continuity the conclusion does hold, and that is A continuous $f \geq 0$ on $[a, b]$ with $\int_{a}^{b} f = 0$ is identically $0$ below.

Claim 2 is stated for $a < b$ and is not orientation-invariant. With the convention of The integral with oriented limits: $\int_{a}^{a} f : = 0$ and $\int_{b}^{a} f : = - \int_{a}^{b} f$ , $f \leq g$ gives $\int_{u}^{v} f \leq \int_{u}^{v} g$ when $u \leq v$ and the reverse inequality when $u \geq v$ , since both sides change sign together.

Facts & Assumptions

Given: Reals $a < b$ and integrable $f, g : [a, b] \to R$ , with reals $m \leq M$ where claim 3 is concerned.

[A1]

$f (x) \geq 0$ for every $x \in [a, b]$ .

[A2]

$f (x) \leq g (x)$ for every $x \in [a, b]$ .

[A3]

$m \leq f (x) \leq M$ for every $x \in [a, b]$ .

[L1]

If $m^{'} \leq h \leq M^{'}$ on $[a, b]$ then $m^{'} (b - a) \leq L (h, P) \leq \underline{\int_{a}^{b}} h \leq \overline{\int_{a}^{b}} h \leq U (h, P) \leq M^{'} (b - a)$ for every partition $P$ (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)$ , 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}$ , Finite sums and finite products, by recursion, Laws of finite sums and finite products).

[L2]

If $h$ is integrable then $\int_{a}^{b} h$ is the common value of the lower and upper integrals (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$ , Greatest lower bound (infimum)).

[L3]

Sums and scalar multiples of integrable functions are integrable, and $\int_{a}^{b} (λ h + ν k) = λ \int_{a}^{b} h + ν \int_{a}^{b} k$ (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]

Ordered-field arithmetic: adding a constant to both sides of an inequality preserves it, and the order is total and transitive (Ordered field, Complete ordered field (least-upper-bound property)). The nonstrict forms follow from the strict ones by adjoining the case of equality.

Proof

technique · direct

1.1

Claim 1. Under [A1] the constant $0$ is a lower bound of $f$ on $[a, b]$ , so [L1] applies with $m^{'} : = 0$ and gives $\underline{\int_{a}^{b}} f \geq 0$ .

A1L1

1.2

Claim 2. Under [A2] the function $h : = g - f$ satisfies $h (x) \geq 0$ for every $x \in [a, b]$ , and $h$ is integrable with $\int_{a}^{b} h = \int_{a}^{b} g - \int_{a}^{b} f$ by [L3].

A2L3L4

2.1

Since $f$ is integrable, $\int_{a}^{b} f = \underline{\int_{a}^{b}} f \geq 0$ by [L2].

step 1.1L2

3.1

By claim 1 applied to $h$ , $\int_{a}^{b} g - \int_{a}^{b} f \geq 0$ , that is $\int_{a}^{b} f \leq \int_{a}^{b} g$ .

step 2.1step 1.2L4

4.1

Claim 3. Under [A3], [L1] applied to $f$ with $m^{'} : = m$ and $M^{'} : = M$ gives $m (b - a) \leq \underline{\int_{a}^{b}} f$ and $\overline{\int_{a}^{b}} f \leq M (b - a)$ , and both integrals equal $\int_{a}^{b} f$ by [L2].

A3L1L2∎

Remarks

Claim 3 is cited, not reproved. 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)$ already proves the five-term chain for every partition, and it is the item that also computes the integral of a constant, $\int_{a}^{b} c = c (b - a)$ . Claim 3 is that chain read at an integrable $f$ ; nothing new is established here.
Claim 2 is proved through claim 1 and linearity, and not by comparing Darboux sums. Comparing sums works too, since $f \leq g$ gives $m_{i} (f) \leq m_{i} (g)$ and $M_{i} (f) \leq M_{i} (g)$ on every subinterval, but the route through $g - f$ is shorter and uses only results already available. Either way the hypothesis is a pointwise inequality on the whole of $[a, b]$ ; an inequality holding off a finite set gives the same conclusion, by Changing an integrable function at finitely many points changes neither its integrability nor its integral, and that is a separate statement.
What claim 2 is for. It is what turns a pointwise estimate on an integrand into an estimate on the integral, and every estimate of that shape on this page and its companion is an application of it. No count of those applications is asserted here; the dependency graph of the page is where that is read off.

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passverified 2026-08-10 (gpt-5.6-terra-codex-subscription)Open item page →

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$

Statement

Let $a < c < b$ be reals and let $f : [a, b] \to R$ be bounded (Lower bound, bounded below, bounded set). Then:

$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$ ) if and only if its restrictions to $[a, c]$ and to $[c, b]$ are integrable;
and in that case $\int_{a}^{b} f = \int_{a}^{c} f + \int_{c}^{b} f .$
Oriented form. Let $α < β$ be reals, let $f : [α, β] \to R$ be integrable, and let $u, v, w \in [α, β]$ be arbitrary. Then, with the convention of The integral with oriented limits: $\int_{a}^{a} f : = 0$ and $\int_{b}^{a} f : = - \int_{a}^{b} f$ , $\int_{u}^{v} f + \int_{v}^{w} f = \int_{u}^{w} f .$

Claim 3 is where The integral with oriented limits: $\int_{a}^{a} f : = 0$ and $\int_{b}^{a} f : = - \int_{a}^{b} f$ earns its place: it holds for every arrangement of the three points, including the degenerate ones, and it is the form used everywhere below.

Facts & Assumptions

Given: Reals $a < c < b$ and a bounded $f : [a, b] \to R$ ; and, for claim 3, reals $α < β$ , an integrable $f : [α, β] \to R$ and points $u, v, w \in [α, β]$ . Let a real $ε > 0$ be given.

[L1]

Riemann's criterion on any closed bounded interval with distinct endpoints (Riemann's criterion: a bounded $f$ on $[a, b]$ is Darboux integrable if and only if for every real $ε > 0$ there is a partition $P$ with $U (f, P) - L (f, P) < ε$ ).

[L2]

A function integrable on $[p, q]$ is integrable on every $[p^{'}, q^{'}] \subseteq [p, q]$ with $p^{'} < q^{'}$ (A function integrable on $[a, b]$ is integrable on every closed subinterval).

[L3]

For a partition $R = (n, t)$ and bounded $h$ : $L (h, R) = \sum_{i < n} m_{i} Δ_{i}$ , $U (h, R) = \sum_{i < n} M_{i} Δ_{i}$ , and $L (h, R) \leq \int_{‾} h \leq \int^{‾} h \leq U (h, R)$ , the integral being the common value of the two when they agree (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$ ).

[L4]

A partition of $[p, q]$ is a pair $(n, t)$ with $n \geq 1$ , $t_{0} = p$ , $t_{i} < t_{i + 1}$ for $i < n$ and $t_{k} = q$ for $k \geq n$ ; its subintervals are $[t_{i}, t_{i + 1}]$ for $i < n$ (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).

[L5]

Finite sums split at an intermediate index, with $\sum_{k = p}^{q - 1} x_{k} = \sum_{j < q - p} x_{p + j}$ (Finite sums and finite products, by recursion, Laws of finite sums and finite products, clause 3).

[L6]

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

[L7]

Ordered-field arithmetic: adding a constant preserves an inequality, the order is total and transitive, and a real of absolute value below every positive real is $0$ (Ordered field, Complete ordered field (least-upper-bound property)).

Proof

technique · direct

1.1

Claim 1, forward. If $f$ is integrable on $[a, b]$ then, since $a < c$ and $c < b$ , [L2] gives integrability on $[a, c]$ and on $[c, b]$ .

1.2

The splice. Let $P_{1} = (n_{1}, t^{1})$ be a partition of $[a, c]$ and $P_{2} = (n_{2}, t^{2})$ one of $[c, b]$ . Define $P : = (n_{1} + n_{2}, t)$ by $t_{i} : = t_{i}^{1}$ for $i \leq n_{1}$ , $t_{n_{1} + j} : = t_{j}^{2}$ for $j \leq n_{2}$ , and $t_{k} : = b$ for $k \geq n_{1} + n_{2}$ . The two prescriptions agree at $i = n_{1}$ , where $t_{n_{1}}^{1} = c = t_{0}^{2}$ ; and $t_{0} = a$ , $t_{n_{1} + n_{2}} = t_{n_{2}}^{2} = b$ , with $t_{i} < t_{i + 1}$ for every $i < n_{1} + n_{2}$ . So $P$ is a partition of $[a, b]$ .

L4construct

1.3

Claim 1, converse. Suppose $f$ is integrable on $[a, c]$ and on $[c, b]$ , and use [L1] on each to fix $P_{1}$ with $U (f, P_{1}) - L (f, P_{1}) < ε \cdot 2^{- 1}$ and $P_{2}$ with $U (f, P_{2}) - L (f, P_{2}) < ε \cdot 2^{- 1}$ .

L1choose

2.1

The first $n_{1}$ subintervals of $P$ are those of $P_{1}$ and the last $n_{2}$ are those of $P_{2}$ , with the matching lengths, so by [L3] and the splitting law [L5], $L (f, P) = L (f, P_{1}) + L (f, P_{2})$ and $U (f, P) = U (f, P_{1}) + U (f, P_{2})$ .

step 1.2L3L4L5

3.1

For the splice $P$ of those two, step 2.1 gives $U (f, P) - L (f, P) < ε$ ; as $ε > 0$ was arbitrary and $f$ is bounded, [L1] makes $f$ integrable on $[a, b]$ .

step 1.2step 2.1step 1.3L1L7

4.1

Claim 2. With $P_{1}$ , $P_{2}$ and $P$ as above, [L3] puts $\int_{a}^{b} f$ between $L (f, P)$ and $U (f, P)$ , that is between $L (f, P_{1}) + L (f, P_{2})$ and $U (f, P_{1}) + U (f, P_{2})$ by step 2.1; and [L3] applied on $[a, c]$ and on $[c, b]$ puts $\int_{a}^{c} f + \int_{c}^{b} f$ between the same two numbers.

step 2.1step 1.3step 3.1L3

5.1

Those two numbers differ by less than $ε$ by step 1.3, so $∣ \int_{a}^{b} f - \int_{a}^{c} f - \int_{c}^{b} f ∣ < ε$ ; as $ε > 0$ was arbitrary the difference is $0$ , which is claim 2.

step 1.3step 4.1L7

6.1

Claim 3, first the sorted case. Let $x \leq y$ in $[α, β]$ . Then $\int_{α}^{y} f = \int_{α}^{x} f + \int_{x}^{y} f$ . Indeed if $α < x < y$ this is claim 2 applied on $[α, y]$ , where $f$ is integrable by [L2]; if $x = α$ the middle term is $0$ by [L6] and the identity is trivial; and if $x = y$ the last term is $0$ by [L6] and the identity is again trivial.

step 5.1L2L6

7.1

Put $F (x) : = \int_{α}^{x} f$ for $x \in [α, β]$ , which is defined by [L2] and [L6]. Then $\int_{x}^{y} f = F (y) - F (x)$ for all $x, y \in [α, β]$ : for $x < y$ this is step 6.1 rearranged; for $x = y$ both sides are $0$ by [L6]; and for $x > y$ the case already proved gives $\int_{y}^{x} f = F (x) - F (y)$ , and [L6] negates both sides.

step 6.1L2L6construct

8.1

Claim 3. For arbitrary $u, v, w \in [α, β]$ , step 7.1 gives $\int_{u}^{v} f + \int_{v}^{w} f = (F (v) - F (u)) + (F (w) - F (v)) = F (w) - F (u) = \int_{u}^{w} f$ .

step 7.1algebra∎

Remarks

The oriented form is not proved by listing six orderings. Step 7.1 shows that the oriented integral between two points is a difference of values of one function of one variable, after which claim 3 is the cancellation $(F (v) - F (u)) + (F (w) - F (v)) = F (w) - F (u)$ , valid however the three points are arranged and however many of them coincide. The case analysis is confined to the two lines of step 7.1, and no appeal to symmetry is made anywhere.
The function $F$ of step 7.1 is the integral function, and it is given its own item, The integral function $F (x) : = \int_{a}^{x} f$ of an integrable $f$ , because the rest of the page is about it. Nothing there re-proves step 7.1; it cites this theorem.
Boundedness on the whole of $[a, b]$ is a hypothesis of claim 1 in both directions. Boundedness on $[a, c]$ and on $[c, b]$ separately does give boundedness on the union, so the converse could be stated with the hypothesis split; it is stated globally because 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}$ needs it globally to make $U (f, P)$ meaningful for a partition of $[a, b]$ .

LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-29Open item page →

Changing an integrable function at finitely many points changes neither its integrability nor its integral

Statement

Let $a < b$ be reals, let $f : [a, b] \to R$ be integrable (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$ ), let $E \subseteq [a, b]$ be finite (Finite, countably infinite, countable, uncountable, Equinumerous sets, $A \approx B$ and $A ⪯ B$ ), and let $g : [a, b] \to R$ satisfy

$g (x) = f (x) for every x \in [a, b] ∖ E .$

Then $g$ is integrable on $[a, b]$ and

$\int_{a}^{b} g = \int_{a}^{b} f .$

In particular the values of an integrand at the endpoints of the interval, and at any finite set of points, are irrelevant to both questions.

Facts & Assumptions

Given: Reals $a < b$ , an integrable $f : [a, b] \to R$ , a finite $E \subseteq [a, b]$ , and $g : [a, b] \to R$ agreeing with $f$ off $E$ . Finite means: there are $r \in N$ and a bijection $e$ from ${j \in N : j < r}$ onto $E$ (Finite, countably infinite, countable, uncountable, Equinumerous sets, $A \approx B$ and $A ⪯ B$ ).

[L1]

Riemann's criterion (Riemann's criterion: a bounded $f$ on $[a, b]$ is Darboux integrable if and only if for every real $ε > 0$ there is a partition $P$ with $U (f, P) - L (f, P) < ε$ ), and: an integrable function is bounded, since Darboux sums are defined only for bounded functions (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).

[L2]

For a partition $R = (n, t)$ and a bounded function $h$ on the interval: $L (h, R) = \sum_{i < n} m_{i} Δ_{i}$ , $U (h, R) = \sum_{i < n} M_{i} Δ_{i}$ with $m_{i} = \inf h [I_{i}] \leq M_{i} = \sup h [I_{i}]$ , and $L (h, R) \leq \underline{\int_{a}^{b}} h \leq \overline{\int_{a}^{b}} h \leq U (h, R)$ (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$ ).

[L3]

The uniform partition $U_{N}$ of $[a, b]$ into $N \geq 1$ parts has $n = N$ and every $Δ_{i}$ equal to $(b - a) / ι (N)$ , and its subintervals cover $[a, b]$ ; the index list $t$ is strictly increasing on indices $\leq N$ , hence injective 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 canonical natural $ι (n) = n \cdot 1_{F}$ of a field, Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length).

[L4]

Finite sums: monotonicity in the terms, scaling, additivity, and splitting; consequently, if $x_{i} = 0$ for every $i < n$ except $i = j$ , then $\sum_{i < n} x_{i} = x_{j}$ , by splitting at $j$ and at $j + 1$ and $\sum 0 = 0$ (Finite sums and finite products, by recursion, Laws of finite sums and finite products, clauses 1 to 4).

[L5]

Sums and scalar multiples of integrable functions are integrable, with the corresponding identity for the integrals (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$ ); and the constant function $0$ is integrable with integral $0$ (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)$ ).

[L6]

For every real $η > 0$ there is a natural $N \geq 1$ with $1 / ι (N) < η$ , and $ι (N) > 0$ for $N \geq 1$ (For every $ε > 0$ in a complete ordered field there is a natural $n \geq 1$ with $1 / n < ε$ , Every complete ordered field is Archimedean, Canonical naturals are positive and strictly increasing).

[L7]

Induction on $N$ (The principle of mathematical induction).

[L8]

Ordered-field arithmetic: multiplying an inequality by a nonnegative quantity and adding constants preserve it, the order is total and transitive, and a real of absolute value below every positive real is $0$ (Ordered field, Complete ordered field (least-upper-bound property)).

Proof

technique · induction

1.1

The one-point case is proved first, for a function called $w$ so that no symbol is reused. Let $p \in [a, b]$ and let $w : [a, b] \to R$ satisfy $w (x) = 0$ for every $x \neq p$ ; put $K : = ∣ w (p) ∣$ , so $∣ w (x) ∣ \leq K$ for every $x$ and $w$ is bounded.

givenL1

1.2

Fix $N \geq 1$ and write $U_{N} = (N, t)$ with subintervals $I_{i}$ and lengths $Δ_{i} = (b - a) / ι (N)$ . Define $θ_{i} : = 1$ if $p \in I_{i}$ and $θ_{i} : = 0$ otherwise, for $i < N$ .

L3construct

1.3

Setting up the induction. Put $h : = g - f$ , so that $h (x) = 0$ for every $x \notin E$ , and for $j < r$ define $h_{j} : [a, b] \to R$ by $h_{j} (x) : = h (x)$ if $x = e (j)$ and $h_{j} (x) : = 0$ otherwise. Each $h_{j}$ vanishes off the single point $e (j)$ .

givenconstruct

2.1

At most two indices $i < N$ have $θ_{i} = 1$ , and they are consecutive: if $p \in I_{i} \cap I_{j}$ with $i < j$ then $t_{j} \leq p \leq t_{i + 1}$ and $t_{i + 1} \leq t_{j}$ , so $t_{i + 1} = t_{j}$ and $j = i + 1$ by injectivity of $t$ . Also some index has $θ_{i} = 1$ , since the subintervals cover $[a, b]$ ; let $i_{0}$ be the least such.

step 1.2L3choose

2.2

For every $x \in [a, b]$ and every $k \leq r$ , $\sum_{j < k} h_{j} (x) = h (x)$ when $x = e (j_{0})$ for some $j_{0} < k$ , and $\sum_{j < k} h_{j} (x) = 0$ otherwise: in the first case all terms with $j \neq j_{0}$ vanish, because $e$ is injective, and [L4] evaluates the sum; in the second every term is $0$ .

step 1.3L4

3.1

For every $i < N$ : if $θ_{i} = 0$ then $w$ vanishes on $I_{i}$ , so $m_{i} = M_{i} = 0$ , where $m_{i}$ and $M_{i}$ are the extreme values of $w$ on $I_{i}$ ; and always $- K θ_{i} \leq m_{i} \leq M_{i} \leq K θ_{i}$ .

step 1.2step 2.1L2L8

3.2

Define $y_{i} : = Δ_{i}$ for $i = i_{0}$ and $y_{i} : = 0$ otherwise, and $z_{i} : = Δ_{i}$ for $i = i_{0} + 1$ with $i_{0} + 1 < N$ , and $z_{i} : = 0$ otherwise. Then $θ_{i} Δ_{i} \leq y_{i} + z_{i}$ for every $i < N$ by step 2.1, and $\sum_{i < N} (y_{i} + z_{i}) \leq 2 (b - a) / ι (N)$ by [L4] and [L3].

step 1.2step 2.1L3L4construct

3.3

Let $Q (k)$ , for $k \leq r$ , be the statement that the function $H_{k} : x \mapsto \sum_{j < k} h_{j} (x)$ is integrable on $[a, b]$ with $\int_{a}^{b} H_{k} = 0$ .

step 2.2construct

4.1

By step 3.1 and monotonicity of finite sums, $U (w, U_{N}) - L (w, U_{N}) = \sum_{i < N} (M_{i} - m_{i}) Δ_{i} \leq \sum_{i < N} 2 K θ_{i} Δ_{i} \leq 4 K (b - a) / ι (N)$ , and likewise $- 2 K (b - a) / ι (N) \leq L (w, U_{N})$ and $U (w, U_{N}) \leq 2 K (b - a) / ι (N)$ .

step 3.1step 3.2L2L4L8

4.2

Base. $H_{0}$ is the constant function $0$ , integrable with integral $0$ by [L5], so $Q (0)$ holds.

basestep 3.3L5

4.3

Induction hypothesis. Fix $k < r$ and assume $Q (k)$ .

ihstep 3.3

5.1

Given a real $η > 0$ , [L6] supplies $N$ with $4 K (b - a) / ι (N) < η$ , so $w$ satisfies Riemann's criterion and is integrable by [L1].

step 4.1L1L6L8

5.2

Moreover $∣ \int_{a}^{b} w ∣ \leq 2 K (b - a) / ι (N)$ for every $N \geq 1$ by step 4.1 and [L2], and the right-hand side is below every positive real by [L6]; hence $\int_{a}^{b} w = 0$ . Steps 1.1 to 5.2 therefore prove: every function on $[a, b]$ vanishing off a single point is integrable with integral $0$ .

step 4.1L2L6L8

6.1

$H_{k + 1} = H_{k} + h_{k}$ pointwise by [L4], and $h_{k}$ is integrable with integral $0$ by steps 5.1 and 5.2 applied to $w : = h_{k}$ and $p : = e (k)$ ; so $H_{k + 1}$ is integrable with $\int_{a}^{b} H_{k + 1} = 0 + 0 = 0$ by [L5], which is $Q (k + 1)$ .

step 5.1step 5.2step 1.3step 4.3L4L5

7.1

By [L7] with steps 4.2 and 6.1, $Q (k)$ holds for every $k \leq r$ ; at $k = r$ , and by step 2.2, $H_{r} = h$ , so $h$ is integrable with $\int_{a}^{b} h = 0$ .

step 2.2step 4.2step 4.3step 6.1L7

8.1

Hence $g = f + h$ is integrable with $\int_{a}^{b} g = \int_{a}^{b} f + 0 = \int_{a}^{b} f$ by [L5].

step 7.1L5discharge-induction∎

Remarks

The subtle point is that a partition point lies in two subintervals. The subintervals of a partition are closed and overlap at their shared endpoints (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), so the exceptional point $p$ may belong to two of them; step 2.1 proves that it belongs to at most two and that they are consecutive, and step 3.2 is what pays for that possibility, with the factor $2$ that survives into step 4.1.
Nothing here is an index-subset sum. The indicator sequence $θ$ of step 1.2 is a genuine sequence on ${i : i < N}$ , and every estimate is applied term by term and then summed by the monotonicity clause of Laws of finite sums and finite products, whose clauses are stated for $\sum_{i < n}$ ; no sum over a subset of the index range is used.
The contrast with the derivative is the point of the lemma. Changing a function at one point can destroy differentiability at that point, and changes nothing at any other point, since a limit at $x \neq p$ may be taken over a neighbourhood excluding $p$ ; it changes no integral at all. This is also why the integral function of an integrable $f$ cannot detect a change of $f$ at a point, which is what FALSE: for every integrable $f$ on $[a, b]$ , the integral function $F (x) = \int_{a}^{x} f$ satisfies $F^{'} = f$ on $[a, b]$ ↗ on the companion page turns into a refutation.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-29Open item page →

If $f$ is integrable on $[a, b]$ with values in $[m, M]$ and $φ$ is continuous on $[m, M]$ , then $φ \circ f$ is integrable

Statement

Let $a < b$ and $m \leq M$ be reals, let $f : [a, b] \to R$ be integrable (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$ ) with

$m \leq f (x) \leq M for every x \in [a, b],$

and let $φ : [m, M] \to R$ be continuous on $[m, M]$ (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). Then the composite $φ \circ f : [a, b] \to R$ is integrable on $[a, b]$ .

The order of the hypotheses is the whole content, and it does not reverse. What is assumed is continuous after integrable: the outer function is the continuous one. Weakening the outer function to a merely integrable $φ$ makes the statement false, and the witness is on the companion page. The remaining variant — $φ$ merely integrable with $f$ continuous — is neither proved nor refuted anywhere on this page, and the companion page's witness does not bear on it, its inner function being discontinuous at every rational. Nothing here asserts anything about that variant.

Facts & Assumptions

Given: Reals $a < b$ and $m \leq M$ , an integrable $f : [a, b] \to R$ with values in $[m, M]$ , a continuous $φ : [m, M] \to R$ , and a real $ε > 0$ . Write $h : = φ \circ f$ .

[L1]

Riemann's criterion: a bounded $u$ on $[a, b]$ is integrable if and only if for every real $η > 0$ there is a partition $P$ with $U (u, P) - L (u, P) < η$ (Riemann's criterion: a bounded $f$ on $[a, b]$ is Darboux integrable if and only if for every real $ε > 0$ there is a partition $P$ with $U (f, P) - L (f, P) < ε$ , 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$ ).

[L2]

For a partition $P = (n, t)$ of $[a, b]$ and bounded $u$ : $U (u, P) - L (u, P) = \sum_{i < n} (M_{i} (u) - m_{i} (u)) Δ_{i}$ with $Δ_{i} > 0$ and $\sum_{i < n} Δ_{i} = b - a$ , and $M_{i} (u) - m_{i} (u) = ω_{u} (I_{i}) = \sup {∣ u (x) - u (y) ∣ : x, y \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}$ , The oscillation $ω_{f} (S) = \sup {∣ f (x) - f (y) ∣ : x, y \in S}$ of $f$ on a set and the oscillation $ω_{f} (c) = \inf_{δ > 0} ω_{f} (A \cap N_{δ} (c))$ at a point, both taken in the extended reals, 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, Finite sums and finite products, by recursion, Laws of finite sums and finite products).

[L3]

$[m, M]$ with $m \leq M$ and $[a, b]$ are closed bounded intervals, hence compact (Heine-Borel by bisection: every closed bounded interval $[a, b]$ is compact, Open cover, subcover, compact subset of $R$ (every open cover has a finite subcover), and sequentially compact subset, Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length).

[L4]

A continuous real function on a compact subset of $R$ is bounded there (A continuous real function on a compact subset of $R$ is bounded, Lower bound, bounded below, bounded set).

[L5]

Heine-Cantor: a continuous real function on a compact $K \subseteq R$ is uniformly continuous on $K$ , so for every real $η > 0$ there is a real $δ_{0} > 0$ with $∣ φ (s) - φ (t) ∣ < η$ for all $s, t \in K$ with $∣ s - t ∣ < δ_{0}$ (Heine-Cantor in $R$ : a continuous real function on a compact subset of $R$ is uniformly continuous, proved $R$ -natively from sequential compactness, Uniform continuity of $f : A \to R$ : one $δ$ serving every pair of points of $A$ ).

[L6]

Finite sums: additivity, scaling and monotonicity in the terms (Finite sums and finite products, by recursion, Laws of finite sums and finite products, clauses 1, 2 and 4).

[L7]

Ordered-field arithmetic and the absolute value: multiplying an inequality by a nonnegative quantity and adding constants preserve it, the order is total and transitive, a positive real has a positive inverse, and $∣ u ∣ \leq c$ follows from $- c \leq u \leq c$ (Ordered field, Complete ordered field (least-upper-bound property), Basic properties of the absolute value). The nonstrict forms follow from the strict ones by adjoining the case of equality.

[L8]

For every real $η > 0$ there is a real $η^{'} > 0$ with $η^{'} < η$ , for instance $η^{'} = η \cdot 2^{- 1}$ ; and the Archimedean property in reciprocal form (For every $ε > 0$ in a complete ordered field there is a natural $n \geq 1$ with $1 / n < ε$ , Every complete ordered field is Archimedean).

Proof

technique · direct

1.1

$[m, M]$ is compact, so $φ$ is bounded there: fix a real $K \geq 0$ with $∣ φ (s) ∣ \leq K$ for every $s \in [m, M]$ . Hence $∣ h (x) ∣ \leq K$ for every $x \in [a, b]$ and $h$ is bounded.

givenL3L4choose

1.2

By [L5] applied on the compact $[m, M]$ with $η : = ε$ , fix a real $δ_{0} > 0$ with $∣ φ (s) - φ (t) ∣ < ε$ whenever $s, t \in [m, M]$ and $∣ s - t ∣ < δ_{0}$ ; then put $δ : = \min {δ_{0} \cdot 2^{- 1}, ε \cdot 2^{- 1}}$ , a positive real with $δ < δ_{0}$ and $δ < ε$ .

givenL3L5L7L8choose

2.1

So $∣ φ (s) - φ (t) ∣ \leq ε$ whenever $s, t \in [m, M]$ satisfy $∣ s - t ∣ \leq δ$ , since $δ < δ_{0}$ .

step 1.2L7

2.2

Since $δ > 0$ , so is $δ^{2}$ , and [L1] supplies a partition $P = (n, t)$ of $[a, b]$ with $U (f, P) - L (f, P) < δ^{2}$ .

step 1.2givenL1L7choose

3.1

Fix $i < n$ and write $Ω_{i} : = M_{i} (f) - m_{i} (f) \geq 0$ . If $Ω_{i} \leq δ$ then any $x, y \in I_{i}$ have $∣ f (x) - f (y) ∣ \leq Ω_{i} \leq δ$ with $f (x), f (y) \in [m, M]$ , so $∣ h (x) - h (y) ∣ \leq ε$ by step 2.1, whence $M_{i} (h) - m_{i} (h) \leq ε$ by [L2].

step 2.1step 2.2L2L7

3.2

If instead $Ω_{i} > δ$ then $Ω_{i} / δ > 1$ , while $M_{i} (h) - m_{i} (h) \leq 2 K$ always, by [L2] and step 1.1.

step 1.1step 2.2L2L7

4.1

In both cases $(M_{i} (h) - m_{i} (h)) Δ_{i} \leq ε Δ_{i} + (2 K / δ) Ω_{i} Δ_{i}$ : in the first case the second summand is nonnegative and the first alone dominates, and in the second case $(2 K / δ) Ω_{i} Δ_{i} \geq 2 K Δ_{i}$ dominates by itself.

step 3.1step 3.2L7

5.1

Summing over $i < n$ with [L6] and using $\sum_{i < n} Δ_{i} = b - a$ and [L2] gives $U (h, P) - L (h, P) \leq ε (b - a) + (2 K / δ) (U (f, P) - L (f, P))$ .

step 4.1L2L6L7

6.1

By step 2.2 the second summand is below $(2 K / δ) δ^{2} = 2 K δ$ , and $δ < ε$ by step 1.2, so $U (h, P) - L (h, P) < ε (b - a + 2 K)$ .

step 2.2step 5.1L7

7.1

Let a real $η > 0$ be given. Running steps 1.2 to 6.1 with $ε : = η / (b - a + 2 K + 1)$ , a positive real since $b - a + 2 K + 1 > 0$ , produces a partition $P$ with $U (h, P) - L (h, P) < η (b - a + 2 K) / (b - a + 2 K + 1) < η$ .

step 6.1L7L8

8.1

As $η > 0$ was arbitrary and $h$ is bounded by step 1.1, [L1] makes $h = φ \circ f$ integrable on $[a, b]$ .

step 1.1step 7.1L1∎

Remarks

Step 4.1 is what replaces the usual split of the index range. The classical proof separates the indices into a good set $G$ and a bad set $B$ and sums over each; the finite-sum toolkit used here is that of Laws of finite sums and finite products, stated for $\sum_{i < n}$ and carrying no clause that splits a range into a subset and its complement, so the split is carried instead by a single inequality valid at every index, whose two summands are exactly the two contributions. The bound obtained is the same one.
The hypothesis $f [[a, b]] \subseteq [m, M]$ is what makes $φ \circ f$ defined at all, and $m, M$ exist because an integrable $f$ is bounded (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}$ ). Taking $[m, M]$ to be any interval containing the range of $f$ is legitimate and changes nothing, since a continuous function on a larger compact interval restricts to a continuous one.
What the theorem does not say. It does not say that $φ \circ f$ is integrable when $φ$ is merely integrable, and it does not say that $\int_{a}^{b} φ \circ f$ can be computed from $\int_{a}^{b} f$ . The first is refuted on the companion page. For the second, take $φ (t) = t^{2}$ on $[0, 1]$ with $f$ the constant $1 / 2$ and with $g$ the indicator of $[0, 1 / 2]$ : both are integrable with integral $1 / 2$ , while $\int_{0}^{1} φ \circ f = 1 / 4$ and $\int_{0}^{1} φ \circ g = 1 / 2$ , so $\int_{a}^{b} φ \circ f$ is not a function of $\int_{a}^{b} f$ .
Forward reference, orientation only. The reversal refuted on the companion page is Integrable $φ$ and integrable $f$ with $φ \circ f$ not integrable: the order of the hypotheses in the composition theorem cannot be reversed ↗; nothing above depends on it.

CorollaryStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-29Open item page →

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

Statement

$∣ f ∣$ , $f^{2}$ and $f g$ are integrable on $[a, b]$ (Absolute value in an ordered field, Integer powers $a^{m}$ );
$\max (f, g)$ and $\min (f, g)$ , defined pointwise (Maximum and minimum of a set), are integrable on $[a, b]$ ;
the triangle inequality for the integral: $∣ \int_{a}^{b} f ∣ \leq \int_{a}^{b} ∣ f ∣ .$

Claim 3 is stated with $a < b$ and is not orientation-invariant. For $u > v$ the right-hand side is $- \int_{v}^{u} ∣ f ∣ \leq 0$ while the left-hand side is $\geq 0$ , so the inequality as written is false there. The form valid for every pair $u, v$ on which $f$ is integrable (The integral with oriented limits: $\int_{a}^{a} f : = 0$ and $\int_{b}^{a} f : = - \int_{a}^{b} f$ ) is

$∣ \int_{u}^{v} f ∣ \leq ∣ \int_{u}^{v} ∣ f ∣ ∣,$

and that is the form the estimates below on this page use whenever the limits are not known to be in increasing order.

The converse of claim 1 fails. Integrability of $∣ f ∣$ does not give integrability of $f$ ; the witness is on the companion page.

Facts & Assumptions

Given: Reals $a < b$ and integrable $f, g : [a, b] \to R$ .

[L1]

If $u$ is integrable on $[a, b]$ with values in $[m, M]$ and $φ$ is continuous on $[m, M]$ , then $φ \circ u$ is integrable (If $f$ is integrable on $[a, b]$ with values in $[m, M]$ and $φ$ is continuous on $[m, M]$ , then $φ \circ f$ is integrable); an integrable function is bounded, so such $m$ and $M$ exist (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, Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length).

[L2]

Sums and scalar multiples of integrable functions are integrable, with $\int_{a}^{b} (λ u + ν w) = λ \int_{a}^{b} u + ν \int_{a}^{b} w$ (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$ ).

[L3]

If $u \leq w$ pointwise on $[a, b]$ and both are integrable then $\int_{a}^{b} u \leq \int_{a}^{b} w$ (If $f \leq g$ on $[a, b]$ and both are integrable then $\int_{a}^{b} f \leq \int_{a}^{b} g$ ; and $m (b - a) \leq \int_{a}^{b} f \leq M (b - a)$ ).

[L4]

The absolute value $t \mapsto ∣ t ∣$ , the square $t \mapsto t^{2}$ and every polynomial function are continuous on every subset of $R$ (Sums, scalar multiples, products, absolute values, maxima, minima and quotients with nonvanishing denominator of continuous functions are continuous, as are constants, the identity and every polynomial function, claims 2 and 5, 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]

For reals $s, t$ : $\max {s, t} = (s + t + ∣ s - t ∣) \cdot 2^{- 1}$ and $\min {s, t} = (s + t - ∣ s - t ∣) \cdot 2^{- 1}$ , and $s t = ((s + t)^{2} - (s - t)^{2}) \cdot 4^{- 1}$ (Maximum and minimum of a set, Absolute value in an ordered field, Ordered field, Integer powers $a^{m}$ ).

[L6]

Absolute value: $- ∣ t ∣ \leq t \leq ∣ t ∣$ , and $∣ t ∣ \leq c$ follows from $- c \leq t \leq c$ (Basic properties of the absolute value, Absolute value in an ordered field).

[L7]

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

[L8]

Ordered-field arithmetic: adding constants and multiplying by positive reals preserve inequalities, and the order is total and transitive (Ordered field, Complete ordered field (least-upper-bound property)).

Proof

technique · direct

1.1

$f$ is bounded, so fix reals $m \leq M$ with $f [[a, b]] \subseteq [m, M]$ ; the same for $g$ , and for $f + g$ and $f - g$ , which are integrable by [L2].

givenL1L2choose

1.2

The maps $t \mapsto ∣ t ∣$ and $t \mapsto t^{2}$ are continuous on any closed bounded interval, by [L4].

2.1

By [L1] applied with $φ (t) = ∣ t ∣$ to $f$ , to $g$ and to $f - g$ , the functions $∣ f ∣$ , $∣ g ∣$ and $∣ f - g ∣$ are integrable.

step 1.1step 1.2L1

2.2

By [L1] applied with $φ (t) = t^{2}$ to $f$ , to $f + g$ and to $f - g$ , the functions $f^{2}$ , $(f + g)^{2}$ and $(f - g)^{2}$ are integrable.

step 1.1step 1.2L1

3.1

By [L5], $f g = ((f + g)^{2} - (f - g)^{2}) \cdot 4^{- 1}$ pointwise, so $f g$ is integrable by [L2]; this completes claim 1.

step 2.1step 2.2L2L5

3.2

By [L5], $\max (f, g) = (f + g + ∣ f - g ∣) \cdot 2^{- 1}$ and $\min (f, g) = (f + g - ∣ f - g ∣) \cdot 2^{- 1}$ pointwise, so both are integrable by [L2]; this is claim 2.

step 2.1L2L5

3.3

Claim 3. By [L6], $- ∣ f ∣ \leq f \leq ∣ f ∣$ pointwise on $[a, b]$ , and all three functions are integrable by step 2.1 and [L2].

step 2.1L2L6

4.1

By [L3] applied twice, $- \int_{a}^{b} ∣ f ∣ \leq \int_{a}^{b} f \leq \int_{a}^{b} ∣ f ∣$ , using $\int_{a}^{b} (- ∣ f ∣) = - \int_{a}^{b} ∣ f ∣$ from [L2].

step 3.3L2L3

5.1

Hence $∣ \int_{a}^{b} f ∣ \leq \int_{a}^{b} ∣ f ∣$ by [L6], which is claim 3.

step 4.1L6

6.1

The oriented form. For $u = v$ both sides are $0$ by [L7]; for $u < v$ it is claim 3 on $[u, v]$ ; and for $u > v$ both $\int_{u}^{v} f$ and $\int_{u}^{v} ∣ f ∣$ are the negatives of the corresponding integrals over $[v, u]$ by [L7], so the two absolute values are unchanged and claim 3 on $[v, u]$ gives the inequality.

step 5.1L7L8∎

Remarks

Every integrability clause comes from one theorem plus linearity. The only input that produces integrability is If $f$ is integrable on $[a, b]$ with values in $[m, M]$ and $φ$ is continuous on $[m, M]$ , then $φ \circ f$ is integrable, with 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$ recombining the pieces; claim 3 additionally uses If $f \leq g$ on $[a, b]$ and both are integrable then $\int_{a}^{b} f \leq \int_{a}^{b} g$ ; and $m (b - a) \leq \int_{a}^{b} f \leq M (b - a)$ , which is the one place an inequality between integrals is needed. The identities of [L5] are algebra, and they are what turns a statement about composing with $∣ \cdot ∣$ and $(\cdot)^{2}$ into statements about products and lattice operations. In particular no new estimate on Darboux sums is made here.
The polarisation identity is used, and it is why $f^{2}$ comes first. There is no direct route from integrability of $f$ and of $g$ to integrability of $f g$ through the composition theorem, because $(s, t) \mapsto s t$ is a function of two variables and the theorem composes with one. Writing $f g$ through squares of sums and differences reduces it to the one-variable case.
The inequality of claim 3 is the integral analogue of the triangle inequality, and like it, it can be strict: for $f (x) = x$ on $[- 1, 1]$ the left-hand side is $0$ and the right-hand side is $1$ .
Forward reference, orientation only. The witness refuting the converse of claim 1 is A function that is not Riemann integrable although $∣ f ∣$ is ↗ on the companion page; nothing above depends on it.

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passverified 2026-08-10 (gpt-5.6-terra-codex-subscription)Open item page →

If $f$ is continuous on $[a, b]$ and $g$ is integrable with $g \geq 0$ , there is $ξ \in [a, b]$ with $\int_{a}^{b} f g = f (ξ) \int_{a}^{b} g$

Statement

Let $a < b$ be reals, let $f : [a, b] \to R$ be continuous on $[a, b]$ (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 let $g : [a, b] \to R$ be integrable (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$ ) with $g (x) \geq 0$ for every $x \in [a, b]$ . Then $f g$ is integrable and there is $ξ \in [a, b]$ with

$\int_{a}^{b} f g = f (ξ) \int_{a}^{b} g .$

The special case $g \equiv 1$ is the familiar statement that a continuous function attains its average value: there is $ξ \in [a, b]$ with

$\int_{a}^{b} f = f (ξ) (b - a),$

and it is this clause that the fundamental theorem below is usually derived from in other treatments.

The hypothesis $g \geq 0$ is essential. For a sign-changing integrable $g$ the conclusion fails, and the witness is the counterexample with a sign-changing weight on the companion page.

Facts & Assumptions

Given: Reals $a < b$ , a continuous $f : [a, b] \to R$ , and an integrable $g : [a, b] \to R$ with $g \geq 0$ on $[a, b]$ .

[L1]

$[a, b]$ is compact, and a continuous real function on a nonempty compact set attains a minimum and a maximum there (Heine-Borel by bisection: every closed bounded interval $[a, b]$ is compact, Open cover, subcover, compact subset of $R$ (every open cover has a finite subcover), and sequentially compact subset, Extreme value theorem: a continuous real function on a nonempty compact subset of $R$ attains a greatest and a least value, Maximum and minimum of a set, Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length).

[L2]

For continuous $f$ on $[a, b]$ with $a \leq b$ , $f [[a, b]] = [\min f [[a, b]], \max f [[a, b]]]$ (The image of an interval under a continuous real function is order-convex, hence an interval, and the image of a closed bounded interval is a closed bounded interval, claim 2).

[L3]

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

[L4]

A product of two integrable functions on $[a, b]$ is integrable (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 ∣$ , claim 1).

[L5]

If $u \leq w$ pointwise and both are integrable then $\int_{a}^{b} u \leq \int_{a}^{b} w$ ; and if $u \geq 0$ is integrable then $\int_{a}^{b} u \geq 0$ (If $f \leq g$ on $[a, b]$ and both are integrable then $\int_{a}^{b} f \leq \int_{a}^{b} g$ ; and $m (b - a) \leq \int_{a}^{b} f \leq M (b - a)$ ).

[L6]

Scalar multiples: $\int_{a}^{b} λ u = λ \int_{a}^{b} u$ (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$ ), and $\int_{a}^{b} 1 = b - a$ (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)$ ).

[L7]

Ordered-field arithmetic: multiplying an inequality by a nonnegative quantity preserves it, a positive real has a positive inverse, and the order is total and transitive (Ordered field, Complete ordered field (least-upper-bound property)).

Proof

technique · direct

1.1

$f$ is integrable by [L3], so $f g$ is integrable by [L4].

givenL3L4

1.2

By [L1] fix $p, q \in [a, b]$ with $f (q) = \min f [[a, b]] = : m$ and $f (p) = \max f [[a, b]] = : M$ , so $m \leq f (x) \leq M$ for every $x \in [a, b]$ .

givenL1choose

1.3

By [L5], $\int_{a}^{b} g \geq 0$ .

givenL5

2.1

Since $g \geq 0$ , multiplying the inequalities of step 1.2 by $g (x)$ gives $m g (x) \leq f (x) g (x) \leq M g (x)$ for every $x \in [a, b]$ , and all three functions are integrable by step 1.1 and [L6].

step 1.1step 1.2givenL6L7

3.1

By [L5] and [L6] applied to step 2.1, $m \int_{a}^{b} g \leq \int_{a}^{b} f g \leq M \int_{a}^{b} g$ .

step 2.1L5L6

4.1

The case $\int_{a}^{b} g = 0$ . Then step 3.1 reads $0 \leq \int_{a}^{b} f g \leq 0$ , so $\int_{a}^{b} f g = 0 = f (a) \int_{a}^{b} g$ , and $ξ : = a$ works.

step 1.3step 3.1L7

4.2

The case $\int_{a}^{b} g > 0$ . Then $λ : = (\int_{a}^{b} f g) / (\int_{a}^{b} g)$ is a real satisfying $m \leq λ \leq M$ , by step 3.1 divided by the positive $\int_{a}^{b} g$ .

step 1.3step 3.1L7construct

5.1

By step 1.2 and [L2], $f [[a, b]] = [m, M]$ , so $λ = f (ξ)$ for some $ξ \in [a, b]$ ; then $\int_{a}^{b} f g = λ \int_{a}^{b} g = f (ξ) \int_{a}^{b} g$ .

step 1.2step 4.2L2L7choose

6.1

The two cases $\int_{a}^{b} g = 0$ and $\int_{a}^{b} g > 0$ are exhaustive by step 1.3, so the theorem holds.

step 1.3step 4.1step 5.1L7

7.1

The clause $g \equiv 1$ . The constant $1$ is integrable, nonnegative, with $\int_{a}^{b} 1 = b - a$ by [L6], so step 6.1 gives $ξ \in [a, b]$ with $\int_{a}^{b} f = f (ξ) (b - a)$ .

step 6.1L6∎

Remarks

The case $\int_{a}^{b} g = 0$ is handled first because the usual proof divides by it. There the conclusion is trivially true for every $ξ$ , and nothing is claimed about the location of a distinguished point; the theorem asserts only that some $ξ$ works.
No intermediate value theorem is invoked directly. What is needed is that the continuous image of $[a, b]$ is exactly $[\min, \max]$ , which is claim 2 of The image of an interval under a continuous real function is order-convex, hence an interval, and the image of a closed bounded interval is a closed bounded interval; that item is itself proved from the intermediate and extreme value theorems, and citing it here saves repeating the argument.
$ξ$ can be forced to lie in the open interval only under extra hypotheses, and none is claimed. The standard refinement puts $ξ$ in the open interval when $g \equiv 1$ ; it is not proved here, it is not needed anywhere on this page, and the theorem does not assert it.
Forward reference, orientation only. The witness showing that $g \geq 0$ cannot be dropped is Continuous $f$ and integrable sign-changing $g$ with $\int_{a}^{b} f g \neq f (ξ) \int_{a}^{b} g$ for every $ξ$ ↗ on the companion page; nothing above depends on it.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (z-ai/glm-5.2)audited 2026-07-29Open item page →

The integral function $F (x) : = \int_{a}^{x} f$ of an integrable $f$

Definition

Let $a < b$ be reals and let $f : [a, b] \to R$ be integrable (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$ ). The integral function of $f$ with base point $a$ is

$F : [a, b] \to R, F (x) : = \int_{a}^{x} f .$

It is a genuine function, and that has to be checked. For $x \in (a, b]$ the restriction of $f$ to $[a, x]$ is integrable, by A function integrable on $[a, b]$ is integrable on every closed subinterval applied with $c : = a$ and $d : = x$ , so $\int_{a}^{x} f$ names a single real number (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$ ). For $x = a$ the symbol $\int_{a}^{a} f$ is $0$ by The integral with oriented limits: $\int_{a}^{a} f : = 0$ and $\int_{b}^{a} f : = - \int_{a}^{b} f$ . So $F (x)$ is defined at every point of $[a, b]$ and

$F (a) = 0.$

More generally, for any base point $c \in [a, b]$ the function $x \mapsto \int_{c}^{x} f$ is defined on the whole of $[a, b]$ , the integral being the oriented one of The integral with oriented limits: $\int_{a}^{a} f : = 0$ and $\int_{b}^{a} f : = - \int_{a}^{b} f$ when $x < c$ ; the case $c = a$ is written $F$ above and is the one used unless another base point is named.

The two identities used throughout

Increments are integrals. For all $x, y \in [a, b]$ , in either order,

$F (y) - F (x) = \int_{x}^{y} f .$

This is claim 3 of 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$ applied to the three points $a$ , $x$ , $y$ : it gives $\int_{a}^{x} f + \int_{x}^{y} f = \int_{a}^{y} f$ , that is $F (x) + \int_{x}^{y} f = F (y)$ . No ordering of $x$ and $y$ is assumed, and the degenerate cases $x = y$ , $x = a$ and $y = a$ are included, since claim 3 is stated for arbitrary points.

Changing the base point changes $F$ by a constant. If $c \in [a, b]$ and $F_{c} (x) : = \int_{c}^{x} f$ , then for every $x \in [a, b]$

$F_{c} (x) = F (x) - F (c),$

again by claim 3 of 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$ at the points $a$ , $c$ , $x$ . So the family of integral functions of $f$ is one function up to an additive constant.

Remarks

$F$ exists for every integrable $f$ , whether or not $f$ has a primitive. Nothing in the definition asks $f$ to be continuous anywhere, and nothing here claims $F^{'} = f$ . The two statements about $F^{'}$ that this page does prove are: $F$ is always Lipschitz (The integral function of a bounded integrable $f$ is Lipschitz, hence uniformly continuous), and $F^{'} (c) = f (c)$ at every point $c$ where $f$ is continuous (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).
$F$ need not be a primitive of $f$ . At a discontinuity of $f$ the derivative $F^{'}$ may fail to exist, or may exist and differ from $f$ ; both possibilities are exhibited on the companion page, by The sign function is Riemann integrable on $[- 1, 1]$ and has no primitive there ↗ and FALSE: for every integrable $f$ on $[a, b]$ , the integral function $F (x) = \int_{a}^{x} f$ satisfies $F^{'} = f$ on $[a, b]$ ↗. That is the honest content of the phrase "the integral function", and it is why it is not called "the primitive" here.
Why the base point is part of the data and the notation suppresses it. The symbol $F$ hides its dependence on $a$ , as is customary; the identity $F_{c} = F - F (c)$ above is what makes the suppression harmless, since every statement below about $F$ is about its increments, which do not see the base point at all.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-29Open item page →

The integral function of a bounded integrable $f$ is Lipschitz, hence uniformly continuous

Statement

Let $a < b$ be reals, let $f : [a, b] \to R$ be integrable (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$ ), let $K \geq 0$ be a real with $∣ f (t) ∣ \leq K$ for every $t \in [a, b]$ (Lower bound, bounded below, bounded set), and let $F$ be the integral function of $f$ (The integral function $F (x) : = \int_{a}^{x} f$ of an integrable $f$ ). Then

$∣ F (y) - F (x) ∣ \leq K ∣ y - x ∣ for all x, y \in [a, b],$

that is, $F$ is Lipschitz with constant $K$ on $[a, b]$ (Lipschitz map, $α$ -Hölder map for rational $0 < α \leq 1$ , and contraction, Dictionary: for $A \subseteq R$ with the metric $d (x, y) = ∣ x - y ∣$ , continuity and uniform continuity of $f : A \to R$ agree with the metric-space notions, the Lipschitz and Hölder conditions are the metric ones instantiated, and a subset of $R$ is compact in the open-cover sense of $R$ exactly when it is a compact metric subspace). Consequently $F$ is uniformly continuous on $[a, b]$ (Uniform continuity of $f : A \to R$ : one $δ$ serving every pair of points of $A$ ) and hence continuous there (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).

No continuity of $f$ is assumed. This is the strongest regularity of $F$ available before the fundamental theorem, and it is what makes the hypotheses of that theorem visible as hypotheses: continuity of $f$ at a point buys differentiability of $F$ there, and integrability alone already buys this much everywhere.

Facts & Assumptions

Given: Reals $a < b$ , an integrable $f : [a, b] \to R$ , a real $K \geq 0$ with $∣ f ∣ \leq K$ on $[a, b]$ , and the integral function $F (x) = \int_{a}^{x} f$ ; points $x, y \in [a, b]$ .

[L1]

$F (y) - F (x) = \int_{x}^{y} f$ for all $x, y \in [a, b]$ , in either order (The integral function $F (x) : = \int_{a}^{x} f$ of an integrable $f$ ).

[L2]

$∣ f ∣$ is integrable on every $[p, q] \subseteq [a, b]$ with $p < q$ , and $∣ \int_{p}^{q} f ∣ \leq \int_{p}^{q} ∣ f ∣$ there (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 ∣$ , claims 1 and 3).

[L3]

If $u \leq w$ pointwise on $[p, q]$ and both are integrable then $\int_{p}^{q} u \leq \int_{p}^{q} w$ , and $\int_{p}^{q} c = c (q - p)$ for a constant $c$ (If $f \leq g$ on $[a, b]$ and both are integrable then $\int_{a}^{b} f \leq \int_{a}^{b} g$ ; and $m (b - a) \leq \int_{a}^{b} f \leq M (b - a)$ , 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)$ ).

[L4]

With oriented limits, $\int_{y}^{x} f = - \int_{x}^{y} f$ and $\int_{x}^{x} f = 0$ (The integral with oriented limits: $\int_{a}^{a} f : = 0$ and $\int_{b}^{a} f : = - \int_{a}^{b} f$ ).

[L5]

Absolute value: $∣ - t ∣ = ∣ t ∣$ , $∣ t ∣ \geq 0$ , and $∣ t ∣ \leq c$ follows from $- c \leq t \leq c$ (Basic properties of the absolute value, Absolute value in an ordered field).

[L6]

A real function on $A \subseteq R$ satisfying $∣ u (x) - u (x^{'}) ∣ \leq L ∣ x - x^{'} ∣$ for all $x, x^{'} \in A$ is Lipschitz with constant $L$ as a map of metric spaces, $R$ carrying its usual metric; a Lipschitz real function is uniformly continuous, and a uniformly continuous one is continuous (Dictionary: for $A \subseteq R$ with the metric $d (x, y) = ∣ x - y ∣$ , continuity and uniform continuity of $f : A \to R$ agree with the metric-space notions, the Lipschitz and Hölder conditions are the metric ones instantiated, and a subset of $R$ is compact in the open-cover sense of $R$ exactly when it is a compact metric subspace, clauses 3 and 6, Lipschitz map, $α$ -Hölder map for rational $0 < α \leq 1$ , and contraction, Contraction implies Lipschitz implies uniformly continuous implies continuous; every Hölder map is uniformly continuous, and a Lipschitz map on a bounded space is Hölder for every exponent, The absolute value makes $R$ a metric space: $d (x, y) = ∣ x - y ∣$ is a metric, its open balls are the intervals $(x - r, x + r)$ , and it is unbounded).

[L7]

Ordered-field arithmetic: the order is total and transitive, and multiplying an inequality by a nonnegative real preserves it (Ordered field, Complete ordered field (least-upper-bound property)).

Proof

technique · direct

1.1

The case $x < y$ . By [L1], $F (y) - F (x) = \int_{x}^{y} f$ , and $[x, y] \subseteq [a, b]$ with $x < y$ .

givenL1

1.2

The case $x = y$ . Then $F (y) - F (x) = 0$ and $K ∣ y - x ∣ = 0$ , so the inequality holds with equality.

L1L4L5

2.1

On $[x, y]$ one has $∣ f (t) ∣ \leq K$ for every $t$ , so by [L2] and [L3], $∣ \int_{x}^{y} f ∣ \leq \int_{x}^{y} ∣ f ∣ \leq \int_{x}^{y} K = K (y - x)$ .

step 1.1givenL2L3

3.1

Hence $∣ F (y) - F (x) ∣ \leq K (y - x) = K ∣ y - x ∣$ when $x < y$ .

step 1.1step 2.1L5

4.1

The case $y < x$ . Applying step 3.1 to the pair $(y, x)$ gives $∣ F (x) - F (y) ∣ \leq K ∣ x - y ∣$ , and $∣ F (y) - F (x) ∣ = ∣ F (x) - F (y) ∣$ with $∣ y - x ∣ = ∣ x - y ∣$ by [L5]; so the inequality holds here too.

step 3.1L5

5.1

The three cases $x < y$ , $x = y$ , $y < x$ are exhaustive by [L7], so $∣ F (y) - F (x) ∣ \leq K ∣ y - x ∣$ for all $x, y \in [a, b]$ .

step 1.2step 3.1step 4.1L7

6.1

By [L6], $F$ is therefore Lipschitz with constant $K$ on $[a, b]$ , hence uniformly continuous on $[a, b]$ , hence continuous there.

step 5.1L6∎

Remarks

The estimate is written out on both sides of the diagonal. Hiding the case $y < x$ inside the absolute value would conceal the fact that $\int_{x}^{y} f$ is then the oriented integral of The integral with oriented limits: $\int_{a}^{a} f : = 0$ and $\int_{b}^{a} f : = - \int_{a}^{b} f$ , and that the published inequality $∣ \int_{p}^{q} f ∣ \leq \int_{p}^{q} ∣ f ∣$ is available only for $p \leq q$ . Step 4.1 is what pays for that.
The constant is any bound on $∣ f ∣$ , and it need not be sharp. If $f$ is integrable then it is bounded by definition of the Darboux sums, so some $K$ exists; the theorem is stated with $K$ given rather than existentially, because every later use supplies its own bound.
The dictionary lemma is cited on purpose. Lipschitz and uniform continuity are defined in this library both for real functions and for maps of metric spaces, and Dictionary: for $A \subseteq R$ with the metric $d (x, y) = ∣ x - y ∣$ , continuity and uniform continuity of $f : A \to R$ agree with the metric-space notions, the Lipschitz and Hölder conditions are the metric ones instantiated, and a subset of $R$ is compact in the open-cover sense of $R$ exactly when it is a compact metric subspace is the single item recording that the two families of notions coincide. Citing it, rather than proving the implication again, is what keeps the library from carrying two notions of continuity.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-29Open item page →

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

Statement

Let $a < b$ be reals, let $f : [a, b] \to R$ be integrable (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$ ), let $F$ be its integral function (The integral function $F (x) : = \int_{a}^{x} f$ of an integrable $f$ ), and let $c \in [a, b]$ be a point at which $f$ is continuous (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). Then $F$ is differentiable at $c$ 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) and

$F^{'} (c) = f (c) .$

At $c = a$ and $c = b$ this is the one-sided statement, which is what 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 means at those points: every point of a nondegenerate interval is a limit point of it, so $F^{'} (c)$ is a meaningful symbol at every $c \in [a, b]$ , and the difference quotient is taken over $[a, b] ∖ {c}$ .

Consequently, if $f$ is continuous on the whole of $[a, b]$ , then $F$ is a primitive of $f$ there: $F^{'} = f$ at every point of $[a, b]$ .

Continuity at $c$ is a hypothesis and it cannot be dropped. For an integrable $f$ that is discontinuous at $c$ , $F^{'} (c)$ may fail to exist, and it may exist and differ from $f (c)$ ; both are exhibited on the companion page, by an integrable function with no primitive and by a false statement about the integral function.

Facts & Assumptions

Given: Reals $a < b$ , an integrable $f : [a, b] \to R$ , its integral function $F (x) = \int_{a}^{x} f$ , a point $c \in [a, b]$ at which $f$ is continuous, and a real $ε > 0$ .

[L1]

$F (x) - F (c) = \int_{c}^{x} f$ for all $x, c \in [a, b]$ , in either order (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]

Continuity at $c$ : for every real $η > 0$ there is a real $δ > 0$ such that every $t \in [a, b]$ with $∣ t - c ∣ < δ$ satisfies $∣ f (t) - f (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]

Every point of a nondegenerate interval is a limit point of it, so $F^{'} (c) = \lim_{x \to c} (F (x) - F (c)) / (x - c)$ is a meaningful symbol, the limit being taken over $[a, b] ∖ {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, The $ε$ - $δ$ limit $\lim_{x \to c} f (x) = L$ of $f : A \to R$ at a limit point $c$ of $A$ , Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length).

[L4]

For $p < q$ in $[a, b]$ : $f$ and $∣ f ∣$ and every constant are integrable on $[p, q]$ ; $\int_{p}^{q} λ = λ (q - p)$ ; sums and scalar multiples of integrable functions are integrable with the corresponding identity; and $∣ \int_{p}^{q} u ∣ \leq \int_{p}^{q} ∣ u ∣$ (A function integrable on $[a, b]$ is integrable on every closed subinterval, 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)$ , 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$ , 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 ∣$ ).

[L5]

If $u \leq w$ pointwise on $[p, q]$ and both are integrable then $\int_{p}^{q} u \leq \int_{p}^{q} w$ (If $f \leq g$ on $[a, b]$ and both are integrable then $\int_{a}^{b} f \leq \int_{a}^{b} g$ ; and $m (b - a) \leq \int_{a}^{b} f \leq M (b - a)$ ).

[L6]

With oriented limits, $\int_{q}^{p} u = - \int_{p}^{q} u$ and $\int_{p}^{p} u = 0$ (The integral with oriented limits: $\int_{a}^{a} f : = 0$ and $\int_{b}^{a} f : = - \int_{a}^{b} f$ ).

[L7]

Absolute value and ordered-field arithmetic: $∣ - t ∣ = ∣ t ∣$ , $∣ t s ∣ = ∣ t ∣ ∣ s ∣$ , $∣ t ∣ \leq c$ follows from $- c \leq t \leq c$ , a positive real has a positive inverse, and the order is total and transitive (Basic properties of the absolute value, Absolute value in an ordered field, Ordered field, Complete ordered field (least-upper-bound property)). The nonstrict forms of the order facts follow from the strict ones by adjoining equality.

[L8]

For every real $η > 0$ there is a real $η^{'} > 0$ with $η^{'} < η$ (For every $ε > 0$ in a complete ordered field there is a natural $n \geq 1$ with $1 / n < ε$ , Every complete ordered field is Archimedean).

Proof

technique · direct

1.1

By [L2] with $η : = ε \cdot 2^{- 1}$ , fix a real $δ > 0$ such that $∣ f (t) - f (c) ∣ < ε \cdot 2^{- 1}$ for every $t \in [a, b]$ with $∣ t - c ∣ < δ$ .

givenL2L7L8choose

1.2

For $x \in [a, b]$ with $x \neq c$ , [L1] and [L4] give $F (x) - F (c) - f (c) (x - c) = \int_{c}^{x} f - \int_{c}^{x} f (c) = \int_{c}^{x} (f (t) - f (c)) d t$ , the constant $f (c)$ having integral $f (c) (x - c)$ over the oriented interval from $c$ to $x$ by [L4] and [L6].

L1L4L6

2.1

The estimate for $c < x < c + δ$ . Every $t \in [c, x]$ has $∣ t - c ∣ < δ$ , so $- ε \cdot 2^{- 1} \leq f (t) - f (c) \leq ε \cdot 2^{- 1}$ there by step 1.1, whence $∣ \int_{c}^{x} (f - f (c)) ∣ \leq ε \cdot 2^{- 1} (x - c)$ by [L4] and [L5].

step 1.1step 1.2L4L5L7

2.2

The estimate for $c - δ < x < c$ . By [L6], $\int_{c}^{x} (f - f (c)) = - \int_{x}^{c} (f - f (c))$ , and every $t \in [x, c]$ has $∣ t - c ∣ < δ$ , so the same argument gives $∣ \int_{c}^{x} (f - f (c)) ∣ \leq ε \cdot 2^{- 1} (c - x)$ .

step 1.1step 1.2L4L5L6L7

3.1

In both cases $∣ \int_{c}^{x} (f - f (c)) ∣ \leq ε \cdot 2^{- 1} ∣ x - c ∣$ , so dividing by the nonzero $∣ x - c ∣$ and using step 1.2 gives $∣ \frac{F (x) - F (c)}{x - c} - f (c) ∣ \leq ε \cdot 2^{- 1} < ε$ for every $x \in [a, b]$ with $0 < ∣ x - c ∣ < δ$ .

step 1.2step 2.1step 2.2L7

4.1

Since $ε > 0$ was arbitrary, the limit of the difference quotient of $F$ at $c$ exists and equals $f (c)$ by [L3]; that is, $F^{'} (c) = f (c)$ .

step 1.1step 3.1L3

5.1

If $f$ is continuous at every point of $[a, b]$ then step 4.1 applies at every $c \in [a, b]$ , so $F^{'} = f$ on $[a, b]$ and $F$ is a primitive of $f$ .

step 4.1L3∎

Remarks

The estimate is written out for $x < c$ as well, and that is not redundancy. For $x < c$ the factor $1 / (x - c)$ is negative and the naive chain $m (x - c) \leq \int_{c}^{x} \leq M (x - c)$ reverses; what makes the argument uniform is taking absolute values before dividing, which is what steps 2.1, 2.2 and 3.1 do. This is the single most common error in this proof.
The route is the definition of the derivative, not the mean value theorem for integrals. Deducing $F^{'} (c) = f (c)$ from If $f$ is continuous on $[a, b]$ and $g$ is integrable with $g \geq 0$ , there is $ξ \in [a, b]$ with $\int_{a}^{b} f g = f (ξ) \int_{a}^{b} g$ would need $f$ continuous on a whole subinterval around $c$ , which is a strictly stronger hypothesis than continuity at the single point $c$ . The theorem as stated is the sharp one.
What is proved at a point is proved at a point. Nothing here says $F$ is differentiable anywhere else, and nothing says $F^{'} = f$ off the continuity set of $f$ . Where $f$ is merely integrable, all that survives is The integral function of a bounded integrable $f$ is Lipschitz, hence uniformly continuous.
Forward references, orientation only. The two failures at a discontinuity are worked out on the companion page as The sign function is Riemann integrable on $[- 1, 1]$ and has no primitive there ↗ and FALSE: for every integrable $f$ on $[a, b]$ , the integral function $F (x) = \int_{a}^{x} f$ satisfies $F^{'} = f$ on $[a, b]$ ↗; nothing above depends on either.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passverified 2026-08-10 (gpt-5.6-terra-codex-subscription)Open item page →

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.

CorollaryStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-29Open item page →

Every continuous function on an interval has a primitive; two primitives differ by a constant; and $\int_{a}^{b} f = G (b) - G (a)$ for any primitive $G$

Statement

Let $I \subseteq R$ be order-convex with at least two elements (Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length) and 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). Call $G : I \to R$ a primitive of $f$ on $I$ when $G$ is differentiable at every point of $I$ as a function on $I$ with $G^{'} = f$ there (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). Then:

Existence. Fix $c_{0} \in I$ . The function $F : I \to R, F (x) : = \int_{c_{0}}^{x} f$ is defined at every $x \in I$ (The integral with oriented limits: $\int_{a}^{a} f : = 0$ and $\int_{b}^{a} f : = - \int_{a}^{b} f$ , The integral function $F (x) : = \int_{a}^{x} f$ of an integrable $f$ ) and is a primitive of $f$ on $I$ .
Uniqueness up to a constant. If $G_{1}$ and $G_{2}$ are primitives of $f$ on $I$ then there is a real $k$ with $G_{1} (x) = G_{2} (x) + k$ for every $x \in I$ .
Evaluation. If $a, b \in I$ with $a < b$ and $G$ is any primitive of $f$ on $I$ , then $\int_{a}^{b} f = G (b) - G (a) .$

The scope is exactly the continuous case, and that is not a limitation of the proof. An integrable function need not have a primitive, and a function with a primitive need not be integrable; this corollary is precisely the intersection where both fundamental theorems apply, and both witnesses are on the companion page.

Facts & Assumptions

Given: An order-convex $I \subseteq R$ with at least two elements, a continuous $f : I \to R$ , a base point $c_{0} \in I$ , and a real $ε > 0$ .

[L1]

A continuous function on a closed bounded interval with distinct endpoints is integrable there; a restriction of a continuous function is continuous (A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion, 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, 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$ ).

[L2]

Order-convexity: if $p, q \in I$ then every real between $p$ and $q$ lies in $I$ , so the closed interval with endpoints $p$ and $q$ is contained in $I$ (Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length).

[L3]

$\int_{p}^{p} u = 0$ , $\int_{q}^{p} u = - \int_{p}^{q} u$ , and for $u$ integrable on a closed bounded interval containing $p, q, r$ one has $\int_{p}^{q} u + \int_{q}^{r} u = \int_{p}^{r} u$ (The integral with oriented limits: $\int_{a}^{a} f : = 0$ and $\int_{b}^{a} f : = - \int_{a}^{b} 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$ , claim 3).

[L4]

First fundamental theorem: if $u$ is integrable on $[p, q]$ with $p < q$ and continuous at $c \in [p, q]$ , then $x \mapsto \int_{p}^{x} u$ has derivative $u (c)$ at $c$ as a function on $[p, q]$ ; written out, for every real $ε > 0$ there is a real $δ > 0$ with $∣ (\int_{p}^{x} u - \int_{p}^{c} u) / (x - c) - u (c) ∣ < ε$ for every $x \in [p, q]$ with $0 < ∣ x - c ∣ < δ$ (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, 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 $ε$ - $δ$ limit $\lim_{x \to c} f (x) = L$ of $f : A \to R$ at a limit point $c$ of $A$ ).

[L5]

Second fundamental theorem: if $H$ is differentiable at every point of $[p, q]$ with $H^{'}$ integrable there, then $\int_{p}^{q} H^{'} = H (q) - H (p)$ (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)$ ).

[L6]

If $u$ is continuous on an order-convex $I$ and differentiable with $u^{'} = 0$ at every interior point of $I$ , then $u$ is constant on $I$ (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).

[L7]

A differentiable function is continuous, and the restriction of a function differentiable at $c$ to a subset still having $c$ as a limit point is differentiable at $c$ with the same derivative; every point of a nondegenerate interval 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, Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length).

[L8]

Ordered-field arithmetic and minima of two reals: the order is total and transitive, and $\min {s, t}$ is a real that is $\leq$ both (Maximum and minimum of a set, Ordered field, Complete ordered field (least-upper-bound property)).

Proof

technique · direct

1.1

$F$ is defined. For $x \in I$ the closed interval with endpoints $c_{0}$ and $x$ lies in $I$ by [L2], $f$ is continuous there, hence integrable when $x \neq c_{0}$ by [L1], and $\int_{c_{0}}^{c_{0}} f = 0$ by [L3]; so $F (x)$ names a real for every $x \in I$ .

givenL1L2L3

1.2

A closed neighbourhood inside $I$ . Fix $c \in I$ . If some element of $I$ is $< c$ , choose $u \in I$ with $u < c$ ; otherwise put $u : = c$ . If some element of $I$ is $> c$ , choose $v \in I$ with $v > c$ ; otherwise put $v : = c$ . Not both $u = c$ and $v = c$ , since $I$ would then have $c$ as its only element; so $u < v$ , and $[u, v] \subseteq I$ by [L2].

givenL2choose

1.3

Claim 2. Let $G_{1}, G_{2}$ be primitives of $f$ on $I$ and put $u : = G_{1} - G_{2}$ . Then $u$ is differentiable at every point of $I$ with $u^{'} = f - f = 0$ there, in particular at every interior point of $I$ , and $u$ is continuous on $I$ by [L7]; so [L6] gives a real $k$ with $u \equiv k$ .

L6L7

2.1

Put $η : = \min {c - u, v - c}$ if $u < c$ and $c < v$ , $η : = v - c$ if $u = c$ , and $η : = c - u$ if $v = c$ ; in every case $η > 0$ .

step 1.2L8construct

2.2

$f$ is integrable on $[u, v]$ by [L1], and for $x \in [u, v]$ , [L3] applied to the points $c_{0}, u, x$ inside the closed interval with endpoints $\min {c_{0}, u}$ and $\max {c_{0}, v}$ , which lies in $I$ by [L2], gives $F (x) = F (u) + \int_{u}^{x} f$ .

step 1.1step 1.2L1L2L3

3.1

Every point of $I$ within $η$ of $c$ lies in $[u, v]$ . Let $x \in I$ with $∣ x - c ∣ < η$ . If $x < c$ then $I$ has an element below $c$ , so $u < c$ and $η \leq c - u$ , whence $x > c - η \geq u$ . If $x > c$ then symmetrically $x < c + η \leq v$ . And $u \leq c \leq v$ covers $x = c$ . So $u \leq x \leq v$ .

step 1.2step 2.1L8

3.2

Hence for $x \in [u, v]$ with $x \neq c$ , $(F (x) - F (c)) / (x - c) = (\int_{u}^{x} f - \int_{u}^{c} f) / (x - c)$ , the constant $F (u)$ cancelling.

step 2.2algebra

3.3

By [L4] applied on $[u, v]$ at the point $c$ , fix a real $δ > 0$ with $∣ (\int_{u}^{x} f - \int_{u}^{c} f) / (x - c) - f (c) ∣ < ε$ for every $x \in [u, v]$ with $0 < ∣ x - c ∣ < δ$ , and put $δ^{'} : = \min {δ, η} > 0$ .

step 2.2givenL1L4L8choose

4.1

Every $x \in I$ with $0 < ∣ x - c ∣ < δ^{'}$ lies in $[u, v]$ by step 3.1, so by step 3.2 and step 3.3, $∣ (F (x) - F (c)) / (x - c) - f (c) ∣ < ε$ .

step 3.1step 3.2step 3.3

5.1

As $ε > 0$ was arbitrary and $c$ is a limit point of $I$ by [L7], $F$ is differentiable at $c$ with $F^{'} (c) = f (c)$ ; since $c \in I$ was arbitrary, $F$ is a primitive of $f$ on $I$ , which is claim 1.

step 1.2step 4.1L7

6.1

Claim 3. Let $a < b$ in $I$ and let $G$ be a primitive of $f$ on $I$ . Then $[a, b] \subseteq I$ by [L2], the restriction of $G$ to $[a, b]$ is differentiable at every point of $[a, b]$ with derivative $f$ there by [L7], and $f$ is integrable on $[a, b]$ by [L1]; so [L5] gives $\int_{a}^{b} f = G (b) - G (a)$ .

L1L2L5L7∎

Remarks

Steps 1.2, 2.1 and 3.1 are the only work beyond citing the two fundamental theorems. 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 is stated on a closed bounded interval, while $I$ here may be open, half-open or unbounded, so the derivative it produces is the derivative of a restriction. What those steps supply is a closed subinterval $[u, v] \subseteq I$ that contains all points of $I$ within $η$ of $c$ , after which the difference quotients of $F$ and of the restriction agree on a punctured neighbourhood and the $ε$ - $δ$ statement transfers verbatim.
"Two primitives differ by a constant" is not re-minted here. 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 already states exactly that, in its second clause, for functions with equal derivatives on an order-convex domain; claim 2 is that statement applied to $G_{1} - G_{2}$ .
Order-convexity of $I$ is essential to claim 2 and harmless elsewhere. On a domain in two pieces a function may be constant on each with different constants, which is why 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 carries the same hypothesis. Claims 1 and 3 use it only to know that closed subintervals spanned by points of $I$ lie in $I$ .
Forward references, orientation only. The two witnesses bounding the scope of this corollary are The sign function is Riemann integrable on $[- 1, 1]$ and has no primitive there ↗ and A function differentiable on $[0, 1]$ whose derivative is unbounded, hence not Riemann integrable ↗ on the companion page; nothing above depends on either.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passverified 2026-08-10 (gpt-5.6-terra-codex-subscription)Open item page →

If $u, v$ are differentiable on $[a, b]$ with $u^{'}, v^{'}$ integrable, then $\int_{a}^{b} u v^{'} = u (b) v (b) - u (a) v (a) - \int_{a}^{b} u^{'} v$

Statement

Let $a < b$ be reals and let $u, v : [a, b] \to R$ be differentiable at every point of $[a, b]$ as functions 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). Suppose $u^{'}$ and $v^{'}$ are 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 $u v^{'}$ and $u^{'} v$ are integrable and

$\int_{a}^{b} u v^{'} = u (b) v (b) - u (a) v (a) - \int_{a}^{b} u^{'} v .$

The integrability of $u^{'}$ and $v^{'}$ is a hypothesis, not a formality. Without it the two integrals in the display need not exist at all, and the identity is then not false but ill-formed; that is the false statement that deletes it on the companion page. The hypothesis is automatic when $u$ and $v$ are continuously differentiable, since a continuous function on $[a, b]$ is integrable (A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion).

Facts & Assumptions

Given: Reals $a < b$ and functions $u, v : [a, b] \to R$ , differentiable at every point of $[a, b]$ , with $u^{'}$ and $v^{'}$ integrable on $[a, b]$ .

[L1]

Product rule: if $u$ and $v$ are differentiable at $c$ then so is $u v$ , with $(u v)^{'} (c) = u^{'} (c) v (c) + u (c) v^{'} (c)$ (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$ , claim 3); every point of $[a, b]$ is a limit point of it, so the rule applies at every point (Limit point, isolated point, adherent point, derived set, and dense subset of $R$ , Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length, 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).

[L2]

A function differentiable at every point of $[a, b]$ is continuous there (A function differentiable at $c$ is continuous at $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]

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

[L4]

[L5]

Sums of integrable functions are integrable, and $\int_{a}^{b} (w_{1} + w_{2}) = \int_{a}^{b} w_{1} + \int_{a}^{b} w_{2}$ (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$ ).

[L6]

If $H$ is differentiable at every point of $[a, b]$ with $H^{'}$ integrable there, then $\int_{a}^{b} H^{'} = H (b) - H (a)$ (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)$ ).

Proof

technique · direct

1.1

$u$ and $v$ are continuous on $[a, b]$ by [L2], hence integrable there by [L3].

givenL2L3

1.2

$u v$ is differentiable at every point of $[a, b]$ with $(u v)^{'} = u^{'} v + u v^{'}$ by [L1].

givenL1

2.1

$u^{'} v$ and $u v^{'}$ are integrable on $[a, b]$ by [L4], being products of the integrable $u^{'}$ with $v$ and of $u$ with the integrable $v^{'}$ .

step 1.1givenL4

3.1

Hence $(u v)^{'} = u^{'} v + u v^{'}$ is integrable by [L5], and $\int_{a}^{b} (u v)^{'} = \int_{a}^{b} u^{'} v + \int_{a}^{b} u v^{'}$ .

step 1.2step 2.1L5

4.1

By [L6] applied to $H : = u v$ , $\int_{a}^{b} (u v)^{'} = u (b) v (b) - u (a) v (a)$ .

step 1.2step 3.1L6

5.1

Comparing steps 3.1 and 4.1 and subtracting $\int_{a}^{b} u^{'} v$ gives $\int_{a}^{b} u v^{'} = u (b) v (b) - u (a) v (a) - \int_{a}^{b} u^{'} v$ .

step 3.1step 4.1algebra∎

Remarks

Step 2.1 is the step usually skipped, and it is why the hypotheses are what they are. The identity is an application of the second fundamental theorem to $u v$ , and that theorem needs $(u v)^{'}$ to be integrable. Integrability of $u^{'}$ and $v^{'}$ plus continuity of $u$ and $v$ delivers it, through the product clause of 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 ∣$ ; nothing weaker is used, and nothing weaker is claimed to suffice.
The boundary term is exactly the increment of $u v$ . Writing the identity as $\int_{a}^{b} u v^{'} + \int_{a}^{b} u^{'} v = (u v) (b) - (u v) (a)$ makes the symmetry in $u$ and $v$ visible and is the form worth remembering.
Discrete counterpart. Abel's summation by parts (Abel summation by parts: with $A_{n} = \sum_{k < n} a_{k}$ one has $\sum_{k < n} a_{k} b_{k} = A_{n} b_{n - 1} - \sum_{k < n - 1} A_{k + 1} (b_{k + 1} - b_{k})$ for every $n \geq 1$ ) is the same manipulation for finite sums, and it is what Bonnet's second mean value theorem: for $f$ monotone and $g$ integrable on $[a, b]$ there is $ξ \in [a, b]$ with $\int_{a}^{b} f g = f (a) \int_{a}^{ξ} g + f (b) \int_{ξ}^{b} g$ below uses in place of this theorem, precisely because that theorem assumes no differentiability.
Forward reference, orientation only. The false statement that deletes the integrability hypothesis is FALSE: if $u$ and $v$ are differentiable on $[a, b]$ then $\int_{a}^{b} u v^{'} = u (b) v (b) - u (a) v (a) - \int_{a}^{b} u^{'} v$ ↗ on the companion page; nothing above depends on it.

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-29Open item page →

Substitution: if $φ$ is differentiable on $[c, d]$ with $φ^{'}$ integrable and $f$ is continuous on an interval containing $φ ([c, d])$ , then $\int_{φ (c)}^{φ (d)} f = \int_{c}^{d} (f \circ φ) φ^{'}$

Statement

Let $c < d$ be reals and let $φ : [c, d] \to R$ be differentiable at every point of $[c, d]$ as a function on $[c, d]$ (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), with $φ^{'}$ integrable on $[c, d]$ (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$ ). Let $J \subseteq R$ be order-convex with at least two elements (Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length) with $φ [[c, d]] \subseteq J$ , and let $f : J \to R$ be continuous on $J$ (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).

Then $(f \circ φ) φ^{'}$ is integrable on $[c, d]$ and

$\int_{φ (c)}^{φ (d)} f = \int_{c}^{d} (f \circ φ) φ^{'},$

the left-hand integral being the oriented one of The integral with oriented limits: $\int_{a}^{a} f : = 0$ and $\int_{b}^{a} f : = - \int_{a}^{b} f$ .

Neither injectivity nor monotonicity of $φ$ is assumed, and that is exactly why the left-hand side is written with oriented limits: $φ (d)$ may lie below $φ (c)$ , and $φ$ may return to the same value many times. The proof runs through a primitive of $f$ and the chain rule, and no inverse function is ever formed.

Continuity of $f$ is a hypothesis and cannot be weakened to integrability. With $f$ merely integrable the composite $f \circ φ$ need not be integrable at all, so the right-hand side need not exist; that is the false statement that weakens it on the companion page.

Facts & Assumptions

Given: Reals $c < d$ , a differentiable $φ : [c, d] \to R$ with $φ^{'}$ integrable, an order-convex $J$ with at least two elements containing $φ [[c, d]]$ , and a continuous $f : J \to R$ .

[L1]

A function differentiable at every point of $[c, d]$ is continuous there, and a continuous function on $[c, d]$ is integrable (A function differentiable at $c$ is continuous at $c$ , A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion, 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).

[L2]

For a continuous $u$ on $[c, d]$ with $c \leq d$ , $u [[c, d]] = [m, M]$ with $m = \min u [[c, d]]$ and $M = \max u [[c, d]]$ (The image of an interval under a continuous real function is order-convex, hence an interval, and the image of a closed bounded interval is a closed bounded interval, claim 2, Maximum and minimum of a set).

[L3]

A continuous function on an order-convex set with at least two elements has a primitive there, two primitives differ by a constant, and $\int_{p}^{q} f = G (q) - G (p)$ for $p < q$ in that set and any primitive $G$ (Every continuous function on an interval has a primitive; two primitives differ by a constant; and $\int_{a}^{b} f = G (b) - G (a)$ for any primitive $G$ ).

[L4]

Chain rule: if $ψ$ is differentiable at $t$ , $ψ (t)$ is a limit point of the domain of $H$ and $H$ is differentiable at $ψ (t)$ , then $H \circ ψ$ is differentiable at $t$ with $(H \circ ψ)^{'} (t) = H^{'} (ψ (t)) ψ^{'} (t)$ ; every point of a nondegenerate order-convex set is a limit point of it (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)$ , Limit point, isolated point, adherent point, derived set, and dense subset of $R$ , Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length, 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).

[L5]

If $w$ is integrable on $[c, d]$ with values in $[m, M]$ and $g$ is continuous on $[m, M]$ then $g \circ w$ is integrable (If $f$ is integrable on $[a, b]$ with values in $[m, M]$ and $φ$ is continuous on $[m, M]$ , then $φ \circ f$ is integrable); a restriction of a continuous function is continuous (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]

A product of two integrable functions on $[c, d]$ is integrable (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 ∣$ , claim 1).

[L7]

If $H$ is differentiable at every point of $[c, d]$ with $H^{'}$ integrable there, then $\int_{c}^{d} H^{'} = H (d) - H (c)$ (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)$ ).

[L8]

With oriented limits, $\int_{q}^{p} f = - \int_{p}^{q} f$ and $\int_{p}^{p} f = 0$ (The integral with oriented limits: $\int_{a}^{a} f : = 0$ and $\int_{b}^{a} f : = - \int_{a}^{b} f$ ).

Proof

technique · direct

1.1

$φ$ is continuous on $[c, d]$ and integrable there by [L1].

givenL1

1.2

By [L3] fix a primitive $F : J \to R$ of $f$ , so $F$ is differentiable at every point of $J$ with $F^{'} = f$ there.

givenL3choose

2.1

By [L2], $φ [[c, d]] = [m, M]$ with $m \leq M$ , and $[m, M] \subseteq J$ by hypothesis.

step 1.1givenL2

2.2

The left-hand side is the same increment. If $φ (c) < φ (d)$ then both lie in $J$ , so $[φ (c), φ (d)] \subseteq J$ and [L3] gives $\int_{φ (c)}^{φ (d)} f = F (φ (d)) - F (φ (c))$ . If $φ (c) = φ (d)$ both sides are $0$ by [L8]. If $φ (c) > φ (d)$ then the case already treated gives $\int_{φ (d)}^{φ (c)} f = F (φ (c)) - F (φ (d))$ , and [L8] negates both sides.

step 1.2L3L8

3.1

For every $t \in [c, d]$ the point $φ (t)$ lies in $J$ , which is a nondegenerate order-convex set, so $φ (t)$ is a limit point of $J$ and [L4] applies: $F \circ φ$ is differentiable at $t$ with $(F \circ φ)^{'} (t) = F^{'} (φ (t)) φ^{'} (t) = f (φ (t)) φ^{'} (t)$ .

step 2.1step 1.2givenL4

3.2

$f$ restricted to $[m, M]$ is continuous, so by [L5] applied to $w : = φ$ the composite $f \circ φ$ is integrable on $[c, d]$ .

step 1.1step 2.1givenL5

4.1

Hence $(f \circ φ) φ^{'}$ is integrable on $[c, d]$ by [L6], $φ^{'}$ being integrable by hypothesis.

step 3.2givenL6

5.1

By [L7] applied to $H : = F \circ φ$ , whose derivative is $(f \circ φ) φ^{'}$ by step 3.1 and is integrable by step 4.1, $\int_{c}^{d} (f \circ φ) φ^{'} = F (φ (d)) - F (φ (c))$ .

step 3.1step 4.1L7

6.1

Comparing steps 5.1 and 2.2 gives $\int_{φ (c)}^{φ (d)} f = \int_{c}^{d} (f \circ φ) φ^{'}$ .

step 5.1step 2.2∎

Remarks

The integral with oriented limits: $\int_{a}^{a} f : = 0$ and $\int_{b}^{a} f : = - \int_{a}^{b} f$ is what makes step 2.2 legal. Without the orientation convention the symbol $\int_{φ (c)}^{φ (d)} f$ would be undefined whenever $φ (d) \leq φ (c)$ , and the theorem would have to carry a monotonicity hypothesis it does not need.
Two integrability facts are checked, not assumed. That $f \circ φ$ is integrable is If $f$ is integrable on $[a, b]$ with values in $[m, M]$ and $φ$ is continuous on $[m, M]$ , then $φ \circ f$ is integrable with the hypotheses in the order that theorem requires — the continuous function is the outer one — and that the product with $φ^{'}$ is integrable is the product clause of 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 ∣$ . Neither is automatic, and the companion page's false statement is exactly the claim that the first of them survives weakening $f$ to an integrable function.
Where the more familiar hypotheses sit. If $φ$ is continuously differentiable then $φ^{'}$ is integrable automatically, and if $φ$ is in addition strictly monotone then the substitution can be read in either direction; neither refinement is needed above, and neither is claimed.
Forward reference, orientation only. The false statement that weakens the continuity of $f$ to integrability is FALSE: in the substitution theorem the continuity of $f$ may be weakened to integrability, $f \circ φ$ still being integrable ↗ on the companion page; nothing above depends on it.

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-29Open item page →

Bonnet's second mean value theorem: for $f$ monotone and $g$ integrable on $[a, b]$ there is $ξ \in [a, b]$ with $\int_{a}^{b} f g = f (a) \int_{a}^{ξ} g + f (b) \int_{ξ}^{b} g$

Statement

Let $a < b$ be reals, let $f : [a, b] \to R$ be monotone, that is nondecreasing or nonincreasing (Nondecreasing, increasing (strictly increasing), nonincreasing, decreasing, monotone and strictly monotone real functions on a subset of $R$ , with the dictionary to monotone sequences), and let $g : [a, b] \to R$ be integrable (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 $f g$ is integrable and there is $ξ \in [a, b]$ with

$\int_{a}^{b} f g = f (a) \int_{a}^{ξ} g + f (b) \int_{ξ}^{b} g .$

No differentiability and no continuity of $f$ is assumed. A monotone function may be discontinuous at infinitely many points and is still integrable (A monotone function on $[a, b]$ is Riemann integrable: for the uniform partition into $N$ parts the upper minus lower sum telescopes to $∣ f (b) - f (a) ∣ (b - a) / ι (N)$ ), and the proof below uses only that its increments over the subintervals of a partition all have the same sign. This is the general form; the version usually proved by integration by parts needs $f$ continuously differentiable, which is a strictly stronger hypothesis.

Facts & Assumptions

Given: Reals $a < b$ , a monotone $f : [a, b] \to R$ , an integrable $g : [a, b] \to R$ , and a real $ε > 0$ . Write $G (x) : = \int_{a}^{x} g$ for the integral function of $g$ , and fix a real $K \geq 0$ with $∣ g (t) ∣ \leq K$ for every $t \in [a, b]$ .

[L1]

A monotone function on $[a, b]$ is bounded and integrable there (A monotone function on $[a, b]$ is Riemann integrable: for the uniform partition into $N$ parts the upper minus lower sum telescopes to $∣ f (b) - f (a) ∣ (b - a) / ι (N)$ , Nondecreasing, increasing (strictly increasing), nonincreasing, decreasing, monotone and strictly monotone real functions on a subset of $R$ , with the dictionary to monotone sequences, Lower bound, bounded below, bounded set); an integrable function is bounded, so $K$ exists (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}$ ).

[L2]

Products of integrable functions are integrable, as are absolute values, and $∣ \int_{p}^{q} u ∣ \leq \int_{p}^{q} ∣ u ∣$ for $p \leq q$ (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]

$G$ is defined on $[a, b]$ , $G (a) = 0$ , $G (y) - G (x) = \int_{x}^{y} g$ for all $x, y \in [a, b]$ in either order, and $G$ is continuous on $[a, b]$ (The integral function $F (x) : = \int_{a}^{x} f$ of an integrable $f$ , The integral function of a bounded integrable $f$ is Lipschitz, hence uniformly continuous, 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$ , The integral with oriented limits: $\int_{a}^{a} f : = 0$ and $\int_{b}^{a} f : = - \int_{a}^{b} f$ , 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).

[L4]

$[a, b]$ is compact and nonempty, so a continuous real function on it attains a minimum and a maximum, and its image is exactly the closed interval between them (Heine-Borel by bisection: every closed bounded interval $[a, b]$ is compact, Open cover, subcover, compact subset of $R$ (every open cover has a finite subcover), and sequentially compact subset, Extreme value theorem: a continuous real function on a nonempty compact subset of $R$ attains a greatest and a least value, The image of an interval under a continuous real function is order-convex, hence an interval, and the image of a closed bounded interval is a closed bounded interval, Maximum and minimum of a set, Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length).

[L5]

Abel summation by parts: with $A_{j} = \sum_{k < j} α_{k}$ , for every $n \geq 1$ one has $\sum_{k < n} α_{k} β_{k} = A_{n} β_{n - 1} - \sum_{k < n - 1} A_{k + 1} (β_{k + 1} - β_{k})$ (Abel summation by parts: with $A_{n} = \sum_{k < n} a_{k}$ one has $\sum_{k < n} a_{k} b_{k} = A_{n} b_{n - 1} - \sum_{k < n - 1} A_{k + 1} (b_{k + 1} - b_{k})$ for every $n \geq 1$ , Series, partial sums, convergence and the sum, divergence, and the tail series).

[L6]

Finite sums: additivity, scaling, splitting with the shift $\sum_{k = p}^{q - 1} x_{k} = \sum_{j < q - p} x_{p + j}$ , monotonicity in the terms, and telescoping $\sum_{k < n} (c_{k + 1} - c_{k}) = c_{n} - c_{0}$ (Finite sums and finite products, by recursion, Laws of finite sums and finite products).

[L7]

For a partition $P = (n, t)$ of $[a, b]$ : $n \geq 1$ , $t_{0} = a$ , $t_{k} = b$ for $k \geq n$ , $Δ_{i} = t_{i + 1} - t_{i} > 0$ for $i < n$ , $I_{i} = [t_{i}, t_{i + 1}] \subseteq [a, b]$ , and $U (f, P) - L (f, P) = \sum_{i < n} (M_{i} - m_{i}) Δ_{i}$ with $m_{i} \leq f (x) \leq M_{i}$ for $x \in I_{i}$ (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, 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}$ ).

[L8]

Riemann's criterion for the integrable $f$ : for every real $η > 0$ there is a partition $P$ with $U (f, P) - L (f, P) < η$ (Riemann's criterion: a bounded $f$ on $[a, b]$ is Darboux integrable if and only if for every real $ε > 0$ there is a partition $P$ with $U (f, P) - L (f, P) < ε$ ).

[L9]

Linearity and monotonicity of the integral, and $\int_{p}^{q} c = c (q - p)$ for a constant (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$ , If $f \leq g$ on $[a, b]$ and both are integrable then $\int_{a}^{b} f \leq \int_{a}^{b} g$ ; and $m (b - a) \leq \int_{a}^{b} f \leq M (b - a)$ , 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)$ ).

[L10]

Absolute value and ordered-field arithmetic: $- c \leq x \leq c$ is equivalent to $∣ x ∣ \leq c$ , multiplying an inequality by a positive real preserves it and by a negative real reverses it, the order is total and transitive, and a real that is $\leq M + η$ for every real $η > 0$ is $\leq M$ (Basic properties of the absolute value, Absolute value in an ordered field, Ordered field, Complete ordered field (least-upper-bound property)).

Proof

technique · direct

1.1

$f$ is bounded and integrable by [L1], so $f g$ is integrable by [L2]; put $Ψ (x) : = \int_{a}^{x} f g$ , so $Ψ (b) = \int_{a}^{b} f g$ and $Ψ (y) - Ψ (x) = \int_{x}^{y} f g$ by [L3] applied to $f g$ .

givenL1L2L3

1.2

$G$ is continuous on $[a, b]$ , so by [L4] there are $m \leq M$ with $G [[a, b]] = [m, M]$ , $m = \min G [[a, b]]$ and $M = \max G [[a, b]]$ .

L3L4choose

1.3

Put $C : = f (b) - f (a)$ and, for a partition $P = (n, t)$ of $[a, b]$ , put $d_{j} : = f (t_{j + 1}) - f (t_{j})$ for $j < n$ . By [L6], $\sum_{j < n} d_{j} = f (t_{n}) - f (t_{0}) = C$ ; and all the $d_{j}$ are $\geq 0$ when $f$ is nondecreasing and all are $\leq 0$ when $f$ is nonincreasing, by [L7] and Nondecreasing, increasing (strictly increasing), nonincreasing, decreasing, monotone and strictly monotone real functions on a subset of $R$ , with the dictionary to monotone sequences.

givenL6L7construct

2.1

The case $C = 0$ . Then $f (a) = f (b)$ , and monotonicity forces $f (x) = f (a)$ for every $x \in [a, b]$ , since $f (x)$ lies between $f (a)$ and $f (b)$ ; so $\int_{a}^{b} f g = f (a) \int_{a}^{b} g$ by [L9], while the right-hand side at $ξ : = a$ is $f (a) \cdot 0 + f (b) \int_{a}^{b} g = f (a) \int_{a}^{b} g$ by [L3]. The theorem holds with $ξ = a$ .

step 1.1step 1.3L3L9L10

2.2

Abel summation on a partition. Let $P = (n, t)$ be any partition of $[a, b]$ . Apply [L5] with $α_{k} : = G (t_{k + 1}) - G (t_{k})$ and $β_{k} : = f (t_{k + 1})$ , noting $t_{k} \in [a, b]$ for every $k \in N$ by [L7]. By [L6], $A_{j} = \sum_{k < j} (G (t_{k + 1}) - G (t_{k})) = G (t_{j}) - G (t_{0}) = G (t_{j})$ , since $G (a) = 0$ .

step 1.2L3L5L6L7

2.3

$S (P)$ approximates $\int_{a}^{b} f g$ . For $k < n$ one has $G (t_{k + 1}) - G (t_{k}) = \int_{t_{k}}^{t_{k + 1}} g$ by [L3], so by [L9] the $k$ -th term of $Ψ (t_{k + 1}) - Ψ (t_{k}) - f (t_{k + 1}) (G (t_{k + 1}) - G (t_{k}))$ equals $\int_{t_{k}}^{t_{k + 1}} (f - f (t_{k + 1})) g$ .

step 1.1L3L9

3.1

So, writing $S (P) : = \sum_{k < n} (G (t_{k + 1}) - G (t_{k})) f (t_{k + 1})$ , [L5] gives $S (P) = G (t_{n}) f (t_{n}) - \sum_{k < n - 1} G (t_{k + 1}) (f (t_{k + 2}) - f (t_{k + 1})) = G (b) f (b) - \sum_{k < n - 1} x_{k + 1}$ , where $x_{j} : = G (t_{j}) d_{j}$ .

step 2.2L5L7construct

3.2

For $x \in I_{k}$ both $f (x)$ and $f (t_{k + 1})$ lie in $[m_{k}, M_{k}]$ , so $∣ (f (x) - f (t_{k + 1})) g (x) ∣ \leq K (M_{k} - m_{k})$ ; hence by [L2] and [L9], $- K (M_{k} - m_{k}) Δ_{k} \leq \int_{t_{k}}^{t_{k + 1}} (f - f (t_{k + 1})) g \leq K (M_{k} - m_{k}) Δ_{k}$ .

step 2.3givenL2L7L9L10

4.1

By [L6], $\sum_{j < n} x_{j} = x_{0} + \sum_{k < n - 1} x_{k + 1}$ , and $x_{0} = G (t_{0}) d_{0} = G (a) d_{0} = 0$ ; so, putting $T (P) : = \sum_{j < n} G (t_{j}) d_{j}$ , step 3.1 reads $S (P) = G (b) f (b) - T (P)$ .

step 3.1L3L6construct

4.2

Summing over $k < n$ with [L6], and telescoping $\sum_{k < n} (Ψ (t_{k + 1}) - Ψ (t_{k})) = Ψ (b) - Ψ (a) = \int_{a}^{b} f g$ , gives $∣ \int_{a}^{b} f g - S (P) ∣ \leq K (U (f, P) - L (f, P))$ .

step 1.1step 2.3step 3.2L6L7L10

5.1

$T (P)$ is $λ_{P} C$ for some $λ_{P} \in [m, M]$ , when $C \neq 0$ . By step 1.2, $m \leq G (t_{j}) \leq M$ for every $j$ . If $f$ is nondecreasing then $d_{j} \geq 0$ , so $m d_{j} \leq G (t_{j}) d_{j} \leq M d_{j}$ , and summing with [L6] and step 1.3 gives $m C \leq T (P) \leq M C$ with $C \geq 0$ ; if $f$ is nonincreasing then $d_{j} \leq 0$ , so $M d_{j} \leq G (t_{j}) d_{j} \leq m d_{j}$ , and summing gives $M C \leq T (P) \leq m C$ with $C \leq 0$ . Dividing by $C$ in the first case, and by the negative $C$ with the inequalities reversed in the second, gives $m \leq T (P) / C \leq M$ in both.

step 1.2step 1.3step 4.1L6L10construct

6.1

The case $C \neq 0$ . Put $λ : = (G (b) f (b) - \int_{a}^{b} f g) / C$ . By step 4.1, $\int_{a}^{b} f g - S (P) = \int_{a}^{b} f g - G (b) f (b) + T (P) = (λ_{P} - λ) C$ for every partition $P$ , where $λ_{P} = T (P) / C$ .

step 4.1step 5.1L10construct

7.1

By [L8] fix a partition $P$ with $U (f, P) - L (f, P) < ε ∣ C ∣ / (K + 1)$ , a positive real; then step 4.2 and step 6.1 give $∣ λ_{P} - λ ∣ ∣ C ∣ \leq K (U (f, P) - L (f, P)) < ε ∣ C ∣$ , so $∣ λ_{P} - λ ∣ < ε$ .

step 4.2step 6.1L8L10choose

8.1

Since $m \leq λ_{P} \leq M$ by step 5.1, it follows that $m - ε < λ < M + ε$ ; as $ε > 0$ was arbitrary, $m \leq λ \leq M$ .

step 5.1step 7.1L10

9.1

By step 1.2, $G [[a, b]] = [m, M]$ , so there is $ξ \in [a, b]$ with $G (ξ) = λ$ .

step 1.2step 8.1L4choose

10.1

Then $\int_{a}^{b} f g = G (b) f (b) - λ C = f (b) G (b) - G (ξ) (f (b) - f (a)) = f (a) G (ξ) + f (b) (G (b) - G (ξ))$ , and $G (ξ) = \int_{a}^{ξ} g$ with $G (b) - G (ξ) = \int_{ξ}^{b} g$ by [L3]; this is the stated identity.

step 6.1step 9.1L3algebra

11.1

The cases $C = 0$ and $C \neq 0$ are exhaustive, so the theorem holds in both.

step 2.1step 10.1L10∎

Remarks

The published summation-by-parts lemma was matched to its own indexing before it was used. Abel summation by parts: with $A_{n} = \sum_{k < n} a_{k}$ one has $\sum_{k < n} a_{k} b_{k} = A_{n} b_{n - 1} - \sum_{k < n - 1} A_{k + 1} (b_{k + 1} - b_{k})$ for every $n \geq 1$ reads $\sum_{k < n} α_{k} β_{k} = A_{n} β_{n - 1} - \sum_{k < n - 1} A_{k + 1} (β_{k + 1} - β_{k})$ with $A_{j} = \sum_{k < j} α_{k}$ , so $A_{0} = 0$ and the boundary value is $β_{n - 1}$ , not $β_{n}$ . Taking $β_{k} : = f (t_{k + 1})$ rather than $f (t_{k})$ is what makes that boundary value $f (t_{n}) = f (b)$ ; and the shifted sum on the right is a sum over $j = 1, \dots, n - 1$ whose missing $j = 0$ term is $G (t_{0}) d_{0} = 0$ , because the integral function vanishes at its base point. Both observations are step 3.1 and step 4.1, and the theorem would be off by a term without either.
The passage to the limit is an estimate, not a Riemann-sum convergence theorem. Step 4.2 bounds $∣ \int_{a}^{b} f g - S (P) ∣$ by $K (U (f, P) - L (f, P))$ for every partition, and the integrability of $f$ alone drives the right-hand side to $0$ . No tagged partition, no mesh condition and no appeal to The Darboux and Riemann definitions agree: a bounded $f$ on $[a, b]$ is Darboux integrable with integral $I$ if and only if for every real $ε > 0$ there is a real $δ > 0$ such that $∣ S (f, P, ξ) - I ∣ < ε$ for every tagged partition of mesh below $δ$ is involved, and the approximating sums are not Riemann sums of $f g$ .
What is not proved here. Nothing is claimed about $ξ$ lying in the open interval, and nothing about the sharper form in which $f$ is assumed nonnegative and nonincreasing, where the conclusion becomes $\int_{a}^{b} f g = f (a) \int_{a}^{ξ} g$ . That refinement needs the one-sided normalisation of $f$ at $a$ and is not used anywhere on this page.

TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-29Open item page →

A continuous $f \geq 0$ on $[a, b]$ with $\int_{a}^{b} f = 0$ is identically $0$

Statement

Let $a < b$ be reals and let $f : [a, b] \to R$ be continuous on $[a, b]$ (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) with $f (x) \geq 0$ for every $x \in [a, b]$ and

$\int_{a}^{b} f = 0.$

Then $f (x) = 0$ for every $x \in [a, b]$ .

This is the exact repair of a published false statement. Without continuity the conclusion fails: FALSE: a nonnegative Riemann integrable function on $[a, b]$ with $\int_{a}^{b} f = 0$ is identically zero, on the companion page of The Riemann Integral, exhibits a nonnegative integrable function with integral $0$ that is positive at every rational point. The remark there says that the continuous case is true and that its proof was not available at that point in the reading order, because additivity over subintervals had not been proved. It is proved now (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$ ), and this item is that proof.

Facts & Assumptions

Given: Reals $a < b$ and a continuous $f : [a, b] \to R$ with $f \geq 0$ on $[a, b]$ and $\int_{a}^{b} f = 0$ .

[A1]

There is $c \in [a, b]$ with $f (c) > 0$ .

[L1]

$f$ is integrable on $[a, b]$ and on every closed subinterval with distinct endpoints (A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion, A function integrable on $[a, b]$ is integrable on every closed subinterval, 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$ ).

[L2]

Continuity at $c$ : for every real $η > 0$ there is a real $δ > 0$ such that every $x \in [a, b]$ with $∣ x - c ∣ < δ$ satisfies $∣ f (x) - f (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]

Additivity: for $a \leq p \leq q \leq b$ , $\int_{a}^{b} f = \int_{a}^{p} f + \int_{p}^{q} f + \int_{q}^{b} f$ , the degenerate pieces being $0$ (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$ , claim 3, The integral with oriented limits: $\int_{a}^{a} f : = 0$ and $\int_{b}^{a} f : = - \int_{a}^{b} f$ ).

[L4]

If $u \geq 0$ is integrable on $[p, q]$ with $p < q$ then $\int_{p}^{q} u \geq 0$ ; and if $u \geq κ$ there then $\int_{p}^{q} u \geq κ (q - p)$ (If $f \leq g$ on $[a, b]$ and both are integrable then $\int_{a}^{b} f \leq \int_{a}^{b} g$ ; and $m (b - a) \leq \int_{a}^{b} f \leq M (b - a)$ , 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)$ ).

[L5]

Ordered-field arithmetic and minima: the order is total and transitive, $\min {s, t}$ and $\max {s, t}$ are reals lying appropriately, a product of two positive reals is positive, and adding constants preserves inequalities (Maximum and minimum of a set, Ordered field, Complete ordered field (least-upper-bound property), Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length).

Proof

technique · contradiction

1.1

Suppose, for contradiction, that $f$ does not vanish identically; since $f \geq 0$ , this gives $c \in [a, b]$ with $f (c) > 0$ , which is [A1].

assume-contragiven

1.2

By [L2] with $η : = f (c) \cdot 2^{- 1} > 0$ , fix a real $δ > 0$ such that every $x \in [a, b]$ with $∣ x - c ∣ < δ$ satisfies $∣ f (x) - f (c) ∣ < f (c) \cdot 2^{- 1}$ , hence $f (x) > f (c) \cdot 2^{- 1}$ .

A1L2L5choose

2.1

Put $p : = \max {a, c - δ \cdot 2^{- 1}}$ and $q : = \min {b, c + δ \cdot 2^{- 1}}$ . Then $a \leq p \leq c \leq q \leq b$ , and $[p, q] \subseteq [a, b]$ .

step 1.2A1L5construct

3.1

$p < q$ : indeed $p \leq c \leq q$ , and $p = q$ would force $p = c = q$ , hence $c = \max {a, c - δ \cdot 2^{- 1}}$ and $c = \min {b, c + δ \cdot 2^{- 1}}$ , so $c = a$ and $c = b$ , contradicting $a < b$ .

step 2.1L5

3.2

Every $x \in [p, q]$ satisfies $∣ x - c ∣ \leq δ \cdot 2^{- 1} < δ$ , so $f (x) > f (c) \cdot 2^{- 1}$ there by step 1.2.

step 1.2step 2.1L5

4.1

Hence $\int_{p}^{q} f \geq f (c) \cdot 2^{- 1} (q - p) > 0$ by [L4] and step 3.1.

step 3.1step 3.2L1L4L5

5.1

By [L3] and [L4], $\int_{a}^{b} f = \int_{a}^{p} f + \int_{p}^{q} f + \int_{q}^{b} f \geq \int_{p}^{q} f > 0$ , the first and third pieces being $\geq 0$ because $f \geq 0$ there, or $0$ when degenerate.

step 4.1L1L3L4L5

6.1

This contradicts the hypothesis $\int_{a}^{b} f = 0$ , so no such $c$ exists and $f (x) = 0$ for every $x \in [a, b]$ .

step 5.1givendischarge-contradiction∎

Remarks

The nonnegativity on the two outer pieces is cited, not assumed away. The usual one-line version writes "so $\int_{a}^{b} f \geq \int_{p}^{q} f$ " without saying why; what makes that step legitimate is that $f \geq 0$ on $[a, p]$ and on $[q, b]$ too, so both of those integrals are $\geq 0$ (If $f \leq g$ on $[a, b]$ and both are integrable then $\int_{a}^{b} f \leq \int_{a}^{b} g$ ; and $m (b - a) \leq \int_{a}^{b} f \leq M (b - a)$ ). Without a sign hypothesis outside $[p, q]$ the argument would fail.
The case where $c$ is an endpoint is covered by the construction, not by a case split. Taking $p$ and $q$ as a maximum and a minimum with $a$ and $b$ makes $[p, q]$ a one-sided neighbourhood of $c$ when $c = a$ or $c = b$ , and step 3.1 is what checks that it is still nondegenerate.
Continuity is used only at the single point $c$ . The proof needs no uniform continuity and no continuity anywhere else, so the statement could be sharpened to: a nonnegative integrable $f$ with $\int_{a}^{b} f = 0$ vanishes at every point of continuity. That sharpening is not asserted as a separate clause because nothing on this page uses it.

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-29Open item page →

The integral test: for $f \geq 0$ nonincreasing on $[0, \infty)$ , $\sum_{k} f (k)$ converges if and only if the sequence $(\int_{0}^{N} f)_{N}$ is bounded, with $\int_{0}^{N} f \leq \sum_{k < N} f (k) \leq f (0) + \int_{0}^{N} f$

Statement

Let $f : [0, \infty) \to R$ be nonincreasing (Nondecreasing, increasing (strictly increasing), nonincreasing, decreasing, monotone and strictly monotone real functions on a subset of $R$ , with the dictionary to monotone sequences) with $f (t) \geq 0$ for every $t \geq 0$ . For $N \in N$ write

$J_{N} : = \int_{0}^{N} f,$

which is defined for every $N$ : for $N \geq 1$ the restriction of $f$ to $[0, N]$ is monotone, hence bounded and integrable (A monotone function on $[a, b]$ is Riemann integrable: for the uniform partition into $N$ parts the upper minus lower sum telescopes to $∣ f (b) - f (a) ∣ (b - a) / ι (N)$ ), and $J_{0} = \int_{0}^{0} f = 0$ (The integral with oriented limits: $\int_{a}^{a} f : = 0$ and $\int_{b}^{a} f : = - \int_{a}^{b} f$ ). Here $N$ inside the integral means the canonical natural $ι (N) \in R$ (The canonical natural $ι (n) = n \cdot 1_{F}$ of a field), as everywhere in this library. Let $s_{N} : = \sum_{k < N} f (k)$ be the partial sums of $\sum_{k} f (k)$ (Series, partial sums, convergence and the sum, divergence, and the tail series, Finite sums and finite products, by recursion), the index $k$ ranging over $N$ , which contains $0$ . Then:

The bracket. For every $N \in N$ , $J_{N} \leq s_{N} \leq f (0) + J_{N} .$
The test. $(J_{N})_{N \in N}$ is nondecreasing, and $\sum_{k} f (k)$ converges if and only if the set ${J_{N} : N \in N}$ is bounded above (Lower bound, bounded below, bounded set).

The conclusion is about a sequence of proper integrals, and that is deliberate. This library has not defined $\int_{0}^{\infty} f$ at this point in the reading order — improper integrals are developed on a later page — so the statement that a reader may expect, " $\sum_{k} f (k)$ converges if and only if $\int_{0}^{\infty} f$ converges", is not available and is not made. What is proved is the statement above, which is what that one abbreviates; the later page is where the two are identified.

The index starts at $0$ . Both the sum and the integral begin at $0$ , because $N$ contains $0$ and a sequence is a function on $N$ (Sequences of reals: bounded, eventually, frequently, tails, subsequences). The classical statement, which starts at $1$ , is the statement about the first tail of $\sum_{k} f (k)$ and is not the statement above.

Facts & Assumptions

Given: A nonincreasing $f : [0, \infty) \to R$ with $f \geq 0$ , and the notation $J_{N} = \int_{0}^{N} f$ , $s_{N} = \sum_{k < N} f (k)$ for $N \in N$ .

[L1]

A monotone function on a closed bounded interval with distinct endpoints is bounded and integrable there, as is its restriction to any closed subinterval with distinct endpoints (A monotone function on $[a, b]$ is Riemann integrable: for the uniform partition into $N$ parts the upper minus lower sum telescopes to $∣ f (b) - f (a) ∣ (b - a) / ι (N)$ , A function integrable on $[a, b]$ is integrable on every closed subinterval, Nondecreasing, increasing (strictly increasing), nonincreasing, decreasing, monotone and strictly monotone real functions on a subset of $R$ , with the dictionary to monotone sequences, 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$ ).

[L2]

If $κ \leq u \leq μ$ on $[p, q]$ with $p < q$ and $u$ is integrable there, then $κ (q - p) \leq \int_{p}^{q} u \leq μ (q - p)$ (If $f \leq g$ on $[a, b]$ and both are integrable then $\int_{a}^{b} f \leq \int_{a}^{b} g$ ; and $m (b - a) \leq \int_{a}^{b} f \leq M (b - a)$ , 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)$ ).

[L3]

Additivity over adjacent intervals, in the oriented form valid for arbitrary points (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$ , claim 3, The integral with oriented limits: $\int_{a}^{a} f : = 0$ and $\int_{b}^{a} f : = - \int_{a}^{b} f$ ).

[L4]

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

[L5]

For a sequence $(a_{k})$ of nonnegative reals, the partial sums are nondecreasing and $\sum a_{k}$ converges if and only if the set of partial sums is bounded above (A series of nonnegative terms converges iff its partial sums are bounded, and then the sum is their supremum, Series, partial sums, convergence and the sum, divergence, and the tail series, Sequences of reals: bounded, eventually, frequently, tails, subsequences).

[L6]

$ι (0) = 0$ , $ι (N + 1) = ι (N) + 1$ , and $ι$ is nondecreasing on $N$ (The canonical natural $ι (n) = n \cdot 1_{F}$ of a field, Canonical naturals are positive and strictly increasing).

[L7]

Ordered-field arithmetic: the order is total and transitive, and adding constants preserves inequalities (Ordered field, Complete ordered field (least-upper-bound property), Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length).

Proof

technique · direct

1.1

For $k \in N$ the interval $[ι (k), ι (k + 1)]$ is nondegenerate of length $1$ by [L6], $f$ is integrable on it by [L1], and $f (k + 1) \leq f (t) \leq f (k)$ for every $t$ in it, $f$ being nonincreasing.

givenL1L6

1.2

By [L3] and [L4], $J_{N} = \int_{0}^{N} f = \sum_{k < N} \int_{k}^{k + 1} f$ for every $N \in N$ : writing $Φ (x) : = \int_{0}^{x} f$ , each summand is $Φ (k + 1) - Φ (k)$ and the sum telescopes to $Φ (N) - Φ (0) = J_{N}$ .

L1L3L4L6

1.3

By [L4], $\sum_{k < N} f (k + 1) = s_{N + 1} - f (0)$ , since splitting $s_{N + 1} = \sum_{k < N + 1} f (k)$ at index $1$ gives $f (0) + \sum_{j < N} f (1 + j)$ .

2.1

Hence $f (k + 1) \leq \int_{k}^{k + 1} f \leq f (k)$ for every $k \in N$ , by [L2] with $q - p = 1$ .

step 1.1L2

3.1

Summing step 2.1 over $k < N$ with [L4] gives $\sum_{k < N} f (k + 1) \leq J_{N} \leq \sum_{k < N} f (k) = s_{N}$ , which is the left half of claim 1.

step 2.1step 1.2L4

3.2

$(J_{N})$ is nondecreasing: $J_{N + 1} - J_{N} = \int_{N}^{N + 1} f \geq 0$ by step 1.2 and [L2], since $f \geq 0$ .

step 2.1step 1.2givenL2L7

4.1

So $s_{N + 1} \leq f (0) + J_{N}$ by step 3.1 and step 1.3; and $s_{N} \leq s_{N + 1}$ because $f (N) \geq 0$ , so $s_{N} \leq f (0) + J_{N}$ , which is the right half of claim 1.

step 3.1step 1.3givenL4L7

4.2

If $\sum_{k} f (k)$ converges, then by [L5] the partial sums are bounded above, say $s_{N} \leq S$ for every $N$ , and step 3.1 gives $J_{N} \leq s_{N} \leq S$ ; so the set of $J_{N}$ is bounded above.

step 3.1givenL5L7

5.1

If the set of $J_{N}$ is bounded above, say by a real $B$ , then $s_{N} \leq f (0) + B$ for every $N$ by step 4.1, so the partial sums are bounded above and $\sum_{k} f (k)$ converges by [L5], the terms $f (k)$ being nonnegative.

step 4.1givenL5L7

6.1

Steps 5.1 and 4.2 are the two implications of claim 2, and step 3.2 is its first clause; claim 1 is steps 3.1 and 4.1.

step 3.1step 4.1step 3.2step 5.1step 4.2∎

Remarks

Why the bracket is stated with $f (0)$ and not with a tail. The two sums in step 3.1 differ by exactly the first term $f (0)$ and the last term $f (N)$ ; the clean two-sided statement that survives at every $N \geq 0$ , including $N = 0$ where it reads $0 \leq 0 \leq f (0)$ , is the one displayed in claim 1.
The version beginning at $k = 1$ is a statement about a tail. For the family $(f (k))_{k \geq 1}$ the same argument on $[1, N]$ gives $\int_{1}^{N} f \leq \sum_{k = 1}^{N - 1} f (k) \leq f (1) + \int_{1}^{N} f$ , and convergence of the two series is equivalent by A series converges iff each of its tail series converges, and the sum splits as $s_{N}$ plus the $N$ -th tail. Nothing above silently starts at $1$ , and a reader comparing with a classical text should check which convention that text uses for $N$ .
Monotonicity of $f$ is used exactly twice, in step 1.1, to bracket $f$ on a unit interval by its two endpoint values, and through A monotone function on $[a, b]$ is Riemann integrable: for the uniform partition into $N$ parts the upper minus lower sum telescopes to $∣ f (b) - f (a) ∣ (b - a) / ι (N)$ to know that $f$ is integrable on $[0, N]$ at all. Nonnegativity is used in three named places: to make $(J_{N})$ nondecreasing in step 3.2, to pass from $s_{N + 1}$ to $s_{N}$ in step 4.1, and to apply A series of nonnegative terms converges iff its partial sums are bounded, and then the sum is their supremum, whose own hypothesis is that the terms are nonnegative. No claim is made here about what happens to the test if that hypothesis is dropped.

RemarkRemark: AI-generatedProof: Not applicablejudge pass (deepseek-v4-pro + gpt-5.6-terra)verified 2026-08-10 (gpt-5.6-terra-codex-subscription)‡ rests on unproved materialOpen item page →

Conventions of this page, and which sharpenings of the integral are taken up later in the reading order

This item is the ledger of the page: what "integrable" means here, what the orientation convention costs, what the page spends in choice, and which sharpenings of the integral belong to later pages rather than to this one. It establishes no theorem and serves only as a conventions and reading-order ledger.

1. One integral, under two names

"Integrable" on this page means Darboux integrable in the sense of 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$ , and $\int_{a}^{b} f$ is the common value of the lower and upper Darboux integrals. By The Darboux and Riemann definitions agree: a bounded $f$ on $[a, b]$ is Darboux integrable with integral $I$ if and only if for every real $ε > 0$ there is a real $δ > 0$ such that $∣ S (f, P, ξ) - I ∣ < ε$ for every tagged partition of mesh below $δ$ that is the same class of functions with the same value as Riemann's own definition by tagged partitions of small mesh, so the two words are used interchangeably, as they are in the literature. No other integral is defined or used by a proof on this page or its companion.

2. The orientation convention, and the statements whose form depends on it

The integral with oriented limits: $\int_{a}^{a} f : = 0$ and $\int_{b}^{a} f : = - \int_{a}^{b} f$ extends the notation by $\int_{u}^{u} f : = 0$ and $\int_{u}^{v} f : = - \int_{v}^{u} f$ for $u > v$ . It is notation, not a new integral: the published definition is stated under the standing hypothesis $a < b$ and simply says nothing outside it.

Several statements on this page take their shape from that convention; three are worth naming, and no claim is made that they are the only ones.

Additivity holds for every arrangement of three points. Claim 3 of 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$ is $\int_{u}^{v} f + \int_{v}^{w} f = \int_{u}^{w} f$ with no ordering assumed, and it is what makes The integral function $F (x) : = \int_{a}^{x} f$ of an integrable $f$ 's identity $F (y) - F (x) = \int_{x}^{y} f$ available in either order.
Substitution keeps the limits in the order the map produces them. Substitution: if $φ$ is differentiable on $[c, d]$ with $φ^{'}$ integrable and $f$ is continuous on an interval containing $φ ([c, d])$ , then $\int_{φ (c)}^{φ (d)} f = \int_{c}^{d} (f \circ φ) φ^{'}$ writes $\int_{φ (c)}^{φ (d)} f$ without assuming $φ$ monotone or injective, and $φ (d) < φ (c)$ is allowed.
One inequality is not orientation-invariant, and that is a trap. The estimate $∣ \int_{u}^{v} f ∣ \leq \int_{u}^{v} ∣ f ∣$ of 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 ∣$ is guaranteed only for $u \leq v$ ; at $u > v$ its right-hand side is $\leq 0$ while its left-hand side is $\geq 0$ . The form valid for every pair is $∣ \int_{u}^{v} f ∣ \leq ∣ \int_{u}^{v} ∣ f ∣ ∣$ , and that item states both.

3. What the page spends in choice

Nothing on this page introduces a new use of a choice principle. Every step that instantiates an existential statement does so finitely many times, which is ordinary first-order reasoning. The one place where a reader might expect a selection is 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)$ : the classical proof picks a mean-value point $ξ_{i}$ in each subinterval of a partition and assembles a Riemann sum, and the proof given here does not, deriving instead the per-index inequality $m_{i} Δ_{i} \leq G (t_{i + 1}) - G (t_{i}) \leq M_{i} Δ_{i}$ and summing it. The same discipline is followed in Bonnet's second mean value theorem: for $f$ monotone and $g$ integrable on $[a, b]$ there is $ξ \in [a, b]$ with $\int_{a}^{b} f g = f (a) \int_{a}^{ξ} g + f (b) \int_{ξ}^{b} g$ , where the approximating sums are built from the values of the integral function at the partition points and no tags are chosen.

Choice does enter through published items that name their own cost, and those costs are inherited unchanged, not added to: Heine-Cantor in $R$ : a continuous real function on a compact subset of $R$ is uniformly continuous, proved $R$ -natively from sequential compactness spends countable choice once, and every item here that rests on A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion or on If $f$ is integrable on $[a, b]$ with values in $[m, M]$ and $φ$ is continuous on $[m, M]$ , then $φ \circ f$ is integrable inherits that single use. 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 spends countable choice once in the half that goes from integrability to the discontinuity set being null, and the companion page uses that half; that use too is inherited and not new. The choice ledger of the previous page, What this page costs in choice: Riemann's criterion, the Darboux-Riemann equivalence and integrability of a monotone function are theorems of ZF; integrability of a continuous function inherits the single use of countable choice inside Heine-Cantor; and only the forward half of the Lebesgue criterion spends countable choice, once, at the countable union of null sets, records the costs of the published items themselves.

4. Index conventions

$N$ contains $0$ ; a sequence is a function on $N$ ; and a partition of $[a, b]$ is indexed from $i = 0$ , its first subinterval being $[t_{0}, t_{1}]$ . Consequently The integral test: for $f \geq 0$ nonincreasing on $[0, \infty)$ , $\sum_{k} f (k)$ converges if and only if the sequence $(\int_{0}^{N} f)_{N}$ is bounded, with $\int_{0}^{N} f \leq \sum_{k < N} f (k) \leq f (0) + \int_{0}^{N} f$ is stated with both the sum and the integral beginning at $0$ , and its bracket carries the term $f (0)$ ; the classical form beginning at $1$ is a statement about a tail, and this page does not silently substitute one for the other. A natural number multiplying or dividing a real always stands for its canonical natural.

5. What is taken up later in the reading order

Stated as reading order, and as no claim at all about what this library currently proves.

Higher derivatives, and Taylor's theorem with the integral remainder. The integral remainder is an application of If $u, v$ are differentiable on $[a, b]$ with $u^{'}, v^{'}$ integrable, then $\int_{a}^{b} u v^{'} = u (b) v (b) - u (a) v (a) - \int_{a}^{b} u^{'} v$ and needs derivatives of order $n$ . The later Darboux/L'Hopital/Taylor page proves the Peano, Lagrange, Cauchy and Schlomilch-Roche forms but explicitly excludes the integral remainder. It is therefore absent from the current library, with no later published page assigned to it; this is a statement about the present reading order, not a theorem about Taylor remainders.
Bounded variation and the Riemann–Stieltjes integral. The later bounded-variation page builds total variation, Jordan decomposition and the Riemann–Stieltjes integral. None is available at this point in the reading order, so nothing on the present page uses it.
Improper integrals. $\int_{0}^{\infty} f$ is not defined anywhere in this library at this point in the reading order, which is why The integral test: for $f \geq 0$ nonincreasing on $[0, \infty)$ , $\sum_{k} f (k)$ converges if and only if the sequence $(\int_{0}^{N} f)_{N}$ is bounded, with $\int_{0}^{N} f \leq \sum_{k < N} f (k) \leq f (0) + \int_{0}^{N} f$ concludes with the boundedness of the sequence $(\int_{0}^{N} f)_{N}$ instead. Identifying the two is what that later page is for.
Interchanging a limit with an integral. Pointwise convergence licenses nothing: the companion page's Continuous $f_{n} \to 0$ pointwise on $[0, 1]$ with $\int_{0}^{1} f_{n} = 1$ for every $n$ ↗ exhibits continuous $f_{n} \to 0$ pointwise on $[0, 1]$ with $\int_{0}^{1} f_{n} = 1$ for every $n$ . What repairs it — uniform convergence, or a domination hypothesis — is not proved on this page and nothing here asserts any version of it.

6. Two results a reader will want next, which this library records but does not prove

Both are recorded elsewhere as results the library does not establish, and they are mentioned here for orientation only; nothing on this page or its companion rests on either.

The sharp fundamental theorem of calculus (absolute continuity) ‡ — the sharp form of the fundamental theorem: the absolutely continuous functions are exactly those for which $G^{'}$ exists almost everywhere, $G^{'} \in L^{1}$ , and $G (x) = G (a) + \int_{a}^{x} G^{'}$ for every $x \in [a, b]$ . The two counterexamples on the companion page, The sign function is Riemann integrable on $[- 1, 1]$ and has no primitive there ↗ and A function differentiable on $[0, 1]$ whose derivative is unbounded, hence not Riemann integrable ↗, are precisely the two ways the naive form fails, and that sharp form is the answer.
Dominated convergence theorem ‡ — the theorem that licenses interchanging a limit with an integral under a domination hypothesis, and the natural sequel to the spike counterexample above.

5 · Examples, counterexamples and false statements

None yet.

Properties of the Integral and the Working FTC

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

The integral with oriented limits: ∫aaf:=0∫aa​f:=0 and ∫baf:=−∫abf∫ba​f:=−∫ab​f

Definition

The two consequences used throughout the page

Remarks

A function integrable on [a,b][a,b] is integrable on every closed subinterval

Statement

Facts & Assumptions

Proof

Remarks

Integrable functions on [a,b][a,b] form a set closed under sums and scalar multiples, and ∫ab(λf+μg)=λ∫abf+μ∫abg∫ab​(λf+μg)=λ∫ab​f+μ∫ab​g

Statement

Facts & Assumptions

Proof

Remarks

If f≤gf≤g on [a,b][a,b] and both are integrable then ∫abf≤∫abg∫ab​f≤∫ab​g; and m(b−a)≤∫abf≤M(b−a)m(b−a)≤∫ab​f≤M(b−a)

Statement

Facts & Assumptions

Proof

Remarks

For a<c<ba<c<b: ff is integrable on [a,b][a,b] if and only if it is integrable on [a,c][a,c] and on [c,b][c,b], and then ∫abf=∫acf+∫cbf∫ab​f=∫ac​f+∫cb​f; with the oriented form for arbitrary a,b,ca,b,c

Statement

Facts & Assumptions

Proof

Remarks

Changing an integrable function at finitely many points changes neither its integrability nor its integral

Statement

Facts & Assumptions

Proof

Remarks

If ff is integrable on [a,b][a,b] with values in [m,M][m,M] and φφ is continuous on [m,M][m,M], then φ∘fφ∘f is integrable

Statement

Facts & Assumptions

Proof

Remarks

If f,gf,g are integrable on [a,b][a,b] then so are ∣f∣∣f∣, f2f2, fgfg, max⁡(f,g)max(f,g) and min⁡(f,g)min(f,g), and ∣∫abf∣≤∫ab∣f∣​∫ab​f​≤∫ab​∣f∣

Statement

Facts & Assumptions

Proof

Remarks

If ff is continuous on [a,b][a,b] and gg is integrable with g≥0g≥0, there is ξ∈[a,b]ξ∈[a,b] with ∫abfg=f(ξ)∫abg∫ab​fg=f(ξ)∫ab​g

Statement

Facts & Assumptions

Proof

Remarks

The integral function F(x):=∫axfF(x):=∫ax​f of an integrable ff

Definition

The two identities used throughout

Remarks

The integral function of a bounded integrable ff is Lipschitz, hence uniformly continuous

Statement

Facts & Assumptions

Proof

Remarks

The first fundamental theorem: if ff is integrable on [a,b][a,b] and continuous at cc, then F′(c)=f(c)F′(c)=f(c); in particular a continuous ff has FF as a primitive

Statement

Facts & Assumptions

Proof

Remarks

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)

Statement

Facts & Assumptions

Proof

Remarks

Every continuous function on an interval has a primitive; two primitives differ by a constant; and ∫abf=G(b)−G(a)∫ab​f=G(b)−G(a) for any primitive GG

Statement

Facts & Assumptions

Proof

Remarks

If u,vu,v are differentiable on [a,b][a,b] with u′,v′u′,v′ integrable, then ∫abuv′=u(b)v(b)−u(a)v(a)−∫abu′v∫ab​uv′=u(b)v(b)−u(a)v(a)−∫ab​u′v

Statement

Facts & Assumptions

Proof

Remarks

Substitution: if φφ is differentiable on [c,d][c,d] with φ′φ′ integrable and ff is continuous on an interval containing φ([c,d])φ([c,d]), then ∫φ(c)φ(d)f=∫cd(f∘φ) φ′∫φ(c)φ(d)​f=∫cd​(f∘φ)φ′

Statement

The integral with oriented limits: $\int_{a}^{a} f : = 0$ and $\int_{b}^{a} f : = - \int_{a}^{b} f$

A function integrable on $[a, b]$ is integrable on every closed subinterval

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$

If $f \leq g$ on $[a, b]$ and both are integrable then $\int_{a}^{b} f \leq \int_{a}^{b} g$ ; and $m (b - a) \leq \int_{a}^{b} f \leq M (b - a)$

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$

If $f$ is integrable on $[a, b]$ with values in $[m, M]$ and $φ$ is continuous on $[m, M]$ , then $φ \circ f$ is integrable

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

If $f$ is continuous on $[a, b]$ and $g$ is integrable with $g \geq 0$ , there is $ξ \in [a, b]$ with $\int_{a}^{b} f g = f (ξ) \int_{a}^{b} g$

The integral function $F (x) : = \int_{a}^{x} f$ of an integrable $f$

The integral function of a bounded integrable $f$ is Lipschitz, hence uniformly continuous

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

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

Every continuous function on an interval has a primitive; two primitives differ by a constant; and $\int_{a}^{b} f = G (b) - G (a)$ for any primitive $G$

If $u, v$ are differentiable on $[a, b]$ with $u^{'}, v^{'}$ integrable, then $\int_{a}^{b} u v^{'} = u (b) v (b) - u (a) v (a) - \int_{a}^{b} u^{'} v$

Substitution: if $φ$ is differentiable on $[c, d]$ with $φ^{'}$ integrable and $f$ is continuous on an interval containing $φ ([c, d])$ , then $\int_{φ (c)}^{φ (d)} f = \int_{c}^{d} (f \circ φ) φ^{'}$

Bonnet's second mean value theorem: for $f$ monotone and $g$ integrable on $[a, b]$ there is $ξ \in [a, b]$ with $\int_{a}^{b} f g = f (a) \int_{a}^{ξ} g + f (b) \int_{ξ}^{b} g$

A continuous $f \geq 0$ on $[a, b]$ with $\int_{a}^{b} f = 0$ is identically $0$

The integral test: for $f \geq 0$ nonincreasing on $[0, \infty)$ , $\sum_{k} f (k)$ converges if and only if the sequence $(\int_{0}^{N} f)_{N}$ is bounded, with $\int_{0}^{N} f \leq \sum_{k < N} f (k) \leq f (0) + \int_{0}^{N} f$