Proof of Integrals of Uniform Limits and of Uniformly Convergent Series

Proof of (i). Boundedness. By Pointwise and Uniform Convergence of a Sequence of Real-Valued Maps (ii) with $\varepsilon=1$, which is positive by Rules of Arithmetic and Order in an Ordered Field (vii), choose $K_{0}\in\mathbb{N}$ with $|f_{k}(t)-f(t)|<1$ for all $k\ge K_{0}$ and $t\in[a,b]$, and let $B_{0}\in\mathbb{R}$ satisfy $|f_{K_{0}}(t)|\le B_{0}$ for every $t\in[a,b]$. For $t\in[a,b]$, $|f(t)|\le|f(t)-f_{K_{0}}(t)|+|f_{K_{0}}(t)|\le1+B_{0}$ by Rules of Arithmetic and Order in an Ordered Field (xi) and Rules of Arithmetic and Order in an Ordered Field (x). So $f$ is bounded, and its upper and lower sums are defined.

Integrability. Let $\varepsilon>0$. We choose, in this order, $\eta$, $K$ and a partition $P$. Put $\eta=\varepsilon/(4(b-a))>0$; by Pointwise and Uniform Convergence of a Sequence of Real-Valued Maps (ii) choose $K\in\mathbb{N}$ with $|f_{k}(t)-f(t)|<\eta$ for all $k\ge K$ and $t\in[a,b]$; and by Riemann's Criterion for Integrability, and the Integral Lies between Lower and Upper Sums (i), applied to $f_{K}$, choose a partition $P$ of $[a,b]$ with $U(f_{K},P)-L(f_{K},P)<\varepsilon/2$. For $t\in[a,b]$, $|f_{K}(t)-f(t)|<\eta$ gives $f(t)\le f_{K}(t)+\eta$ and $f_{K}(t)\le f(t)+\eta$ (Rules of Arithmetic and Order in an Ordered Field (x) and Rules of Arithmetic and Order in an Ordered Field (iv)). By Darboux Sums of Sums, Scalar Multiples and Dominated Functions, and the Oscillation Bound (iii), applied to $f,f_{K}$ and to $f_{K},f$ with $c=\eta$, $U(f,P)\le U(f_{K},P)+\eta\,(b-a)$ and $L(f_{K},P)\le L(f,P)+\eta\,(b-a)$. Subtracting, and as $2\eta\,(b-a)=\varepsilon/2$,

$$U(f,P)-L(f,P)\le U(f_{K},P)-L(f_{K},P)+2\eta\,(b-a)<\varepsilon/2+\varepsilon/2=\varepsilon ,$$

using Inequalities in an Ordered Field: Mixed Transitivity, Strict Sums, Signs, Products, Natural Numbers, Halving, Reciprocals, Absolute Values and Squares (ii) and Inequalities in an Ordered Field: Mixed Transitivity, Strict Sums, Signs, Products, Natural Numbers, Halving, Reciprocals, Absolute Values and Squares (vii). As $\varepsilon$ was arbitrary, $f$ is integrable on $[a,b]$ by Riemann's Criterion for Integrability, and the Integral Lies between Lower and Upper Sums (i).

Convergence of the integrals. The map $k\mapsto\int_{a}^{b}f_{k}$ is a sequence in $\mathbb{R}$ (A Predicative Formula for the Oriented Riemann Integral, and Maps Given by Integrals (ii)). Let $\varepsilon>0$. Put $\eta=\varepsilon/(2(b-a))>0$ and, by Pointwise and Uniform Convergence of a Sequence of Real-Valued Maps (ii), choose $K\in\mathbb{N}$ with $|f_{k}(t)-f(t)|<\eta$ for all $k\ge K$ and $t\in[a,b]$. Let $k\ge K$ and let $d_{k}=f_{k}+(-1)f$, formed with the pointwise operations, so $d_{k}(t)=f_{k}(t)-f(t)$ for $t\in[a,b]$ by Pointwise Operations on Real-Valued Maps (i). By Rules for the Riemann Integral: Sums, Scalar Multiples, Monotonicity, Bounds and Constants (ii), $(-1)f$ is bounded and integrable on $[a,b]$ with $\int_{a}^{b}(-1)f=-\int_{a}^{b}f$, and then, by Rules for the Riemann Integral: Sums, Scalar Multiples, Monotonicity, Bounds and Constants (i), $d_{k}$ is bounded and integrable on $[a,b]$ with $\int_{a}^{b}d_{k}=\int_{a}^{b}f_{k}-\int_{a}^{b}f$. As $|d_{k}(t)|\le\eta$ for every $t\in[a,b]$, Rules for the Riemann Integral: Sums, Scalar Multiples, Monotonicity, Bounds and Constants (v) gives

$$\Bigl|\int_{a}^{b}f_{k}-\int_{a}^{b}f\Bigr|\le\eta\,(b-a)=\varepsilon/2<\varepsilon$$

(Inequalities in an Ordered Field: Mixed Transitivity, Strict Sums, Signs, Products, Natural Numbers, Halving, Reciprocals, Absolute Values and Squares (vii)). Hence $\bigl(\int_{a}^{b}f_{k}\bigr)_{k\in\mathbb{N}}$ converges to $\int_{a}^{b}f$ by Convergent Sequences of Real Numbers (i).

Proof of (ii). The maps $s_{n}$ form a sequence $(s_{n})_{n\in\mathbb{N}}$ in $\mathbb{R}^{[a,b]}$ (Sequences of Real-Valued Maps: the Map of Pointwise Limits on a Subset, and the Sequence of Pointwise Partial Sums (ii)). Let $A$ be the set of those $n\in\mathbb{N}$ for which $s_{n}$ is bounded and integrable on $[a,b]$ and $\int_{a}^{b}s_{n}=\sum_{k=1}^{n}\int_{a}^{b}g_{k}$ (A Predicative Formula for the Oriented Riemann Integral, and Maps Given by Integrals (i) and Typed Terms under a Predicative Guard: Variables, Parameters, Values of Maps and Ordered Pairs, and Predicative Equations and Memberships between Them (vii)). By Iterated Operations: Recursion, Splitting, Reordering, Termwise Combination and Homomorphisms (i), $s_{1}(t)=g_{1}(t)$ for every $t\in[a,b]$, so $s_{1}=g_{1}$ (Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (iv)), and $\sum_{k=1}^{1}\int_{a}^{b}g_{k}=\int_{a}^{b}g_{1}$; thus $1\in A$. Let $n\in A$; then $n+1\in\mathbb{N}$ by Natural Numbers Are the Successors in Omega: One Is Least and Not a Successor of a Natural Number, the Successor Is Injective, and N Is Closed under Addition and Multiplication (vi), so $s_{n+1}$ and $g_{n+1}$ are defined. By Iterated Operations: Recursion, Splitting, Reordering, Termwise Combination and Homomorphisms (i), $s_{n+1}(t)=s_{n}(t)+g_{n+1}(t)$ for every $t\in[a,b]$, so $s_{n+1}=s_{n}+g_{n+1}$ by Pointwise Operations on Real-Valued Maps (i). By Rules for the Riemann Integral: Sums, Scalar Multiples, Monotonicity, Bounds and Constants (i), $s_{n+1}$ is bounded and integrable on $[a,b]$ and, using Iterated Operations: Recursion, Splitting, Reordering, Termwise Combination and Homomorphisms (i) again,

$$\int_{a}^{b}s_{n+1}=\int_{a}^{b}s_{n}+\int_{a}^{b}g_{n+1}=\sum_{k=1}^{n}\int_{a}^{b}g_{k}+\int_{a}^{b}g_{n+1}=\sum_{k=1}^{n+1}\int_{a}^{b}g_{k};$$

so $n+1\in A$, as $n+1\in\mathbb{N}$. By Arithmetic and Order of the Natural Numbers (xiii), $A=\mathbb{N}$.

By (i), applied to the sequence $(s_{n})_{n\in\mathbb{N}}$ in $\mathbb{R}^{[a,b]}$ and to $s$, the map $s$ is bounded and integrable on $[a,b]$ and $\bigl(\int_{a}^{b}s_{n}\bigr)_{n\in\mathbb{N}}$ converges to $\int_{a}^{b}s$. Since $\int_{a}^{b}s_{n}=\sum_{k=1}^{n}\int_{a}^{b}g_{k}$ is the $n$-th partial sum of the sequence $\bigl(\int_{a}^{b}g_{k}\bigr)_{k\in\mathbb{N}}$ (A Predicative Formula for the Oriented Riemann Integral, and Maps Given by Integrals (ii)), the series $\sum_{k=1}^{\infty}\int_{a}^{b}g_{k}$ converges by Series of Real Numbers: Partial Sums, Convergence, the Sum and Absolute Convergence (ii), and its sum, the limit of its partial sums, is $\int_{a}^{b}s$, the limit being unique by Limits of Sequences of Real Numbers: Uniqueness, Boundedness, Constants, Tails, Arithmetic, Quotients, Absolute Values, Finite Sums, Order, Squeezing, Domination and Subsequences (ii).