Proof of Kit for def:riemann-integral

Throughout, formulas are written with abbreviations as in Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (vi), a formula being predicative when it is so with its abbreviations eliminated; the given $x_{0},\dots,x_{N-1}$ are the first of distinct set variables $x_{0},x_{1},\dots$ as in Renaming and Substituting Variables in Predicative Formulas, so that $x_{0},\dots,x_{7}$ are distinct also when $N<8$; the parameters, at their fixed values as in Conditions Expressed by a Predicative Formula, and Guards (i), are distinct from $x_{0},x_{1},\dots$, and the bound variables of $\psi_{L}$, $\psi_{U}$ and of the formulas of the cited lemmas are chosen other than $x_{0},\dots,x_{7}$ and the parameters, while bound variables of the formulas built here are renamed where needed so that none is captured, as in Renaming and Substituting Variables in Predicative Formulas (i); and routine facts about maps and sets, among them that real numbers are sets and that a subclass of a set is a set, are used without comment (Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity).

A formula built from predicative formulas by connectives and by quantifiers over set variables is predicative (Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (v)). For a predicative formula $\varphi$ in $x_{0},\dots,x_{m-1}$ and indices $n_{0},\dots,n_{m-1}$, $\varphi(x_{n_{0}},\dots,x_{n_{m-1}})$ is the formula of Renaming and Substituting Variables in Predicative Formulas (i): a predicative formula in $x_{0},\dots,x_{n-1}$, for every $n$ larger than all $n_{r}$, which holds exactly when $\varphi$ holds with the set assigned to $x_{n_{r}}$ assigned to $x_{r}$, $r<m$. Pair memberships $(s,t)\in w$ and equations $p=(s,t)$ are the predicative formulas of Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (iii) and Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (ii); $s\le t$ and $s<t$ stand for the memberships of the pair $(s,t)$ in the parameters $\le$ and $<$ of $\mathbb{R}$ (The Real Line: Standing Notation and Background for Calculus on Intervals (ii)), which hold exactly when $s,t\in\mathbb{R}$ and $s\le t$, respectively $s<t$; and $\mu(F,A,B)$ is the predicative formula of Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (vii), which holds exactly when $F$ is a map $F:A\to B$.

The Darboux formulas. By Predicative Formulas for Upper and Lower Darboux Sums, and the Maps and Sets of Darboux Sums over All Partitions (i), with $x_{0},\dots,x_{4}$ put for its set variables $a$, $b$, $f$, $P$ and $z$ (Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (i)), there are predicative formulas $\psi_{L}$ and $\psi_{U}$ in $x_{0},\dots,x_{4}$, whose parameters are among those of the statement, with the following meaning. For sets $a$, $b$, $f$, $P$ and $s$ assigned to $x_{0},\dots,x_{4}$, $\psi_{L}$ holds if and only if $a,b\in\mathbb{R}$, $a<b$, $f$ is a bounded map $f:[a,b]\to\mathbb{R}$, $P\in\Pi_{a,b}$ and $s=L(f,P)$, the lower sum; and $\psi_{U}$ holds if and only if the same holds with the upper sum $U(f,P)$ in place of $L(f,P)$. By Partitions of a Closed Interval, the Set of Partitions, and Refinements (ii), $P\in\Pi_{a,b}$ means that $P$ is a partition of $[a,b]$.

Integrable functions. In this paragraph $a$, $b$, $f$, $z$, $P$, $s$ and $c$ denote $x_{0},\dots,x_{6}$, and $\psi_{L}(a,b,f,P,s)$ and $\psi_{U}(a,b,f,P,s)$ are $\psi_{L}(x_{0},x_{1},x_{2},x_{4},x_{5})$ and $\psi_{U}(x_{0},x_{1},x_{2},x_{4},x_{5})$. Let

$$\mathrm{Lo}:\quad z\in\mathbb{R}\wedge\exists P\,\exists s\,\psi_{L}(a,b,f,P,s)\wedge\forall P\,\forall s\,\bigl(\psi_{L}(a,b,f,P,s)\Rightarrow s\le z\bigr)\wedge\forall c\,\Bigl(\bigl(c\in\mathbb{R}\wedge\forall P\,\forall s\,(\psi_{L}(a,b,f,P,s)\Rightarrow s\le c)\bigr)\Rightarrow z\le c\Bigr),$$

let $\mathrm{Up}$ be obtained from $\mathrm{Lo}$ by putting $\psi_{U}$ for $\psi_{L}$ and $z\le s$, $c\le s$ and $c\le z$ for $s\le z$, $s\le c$ and $z\le c$, and let

$$\varepsilon=\exists z\,(\mathrm{Lo}\wedge\mathrm{Up}).$$

These formulas are predicative; the free variables of $\mathrm{Lo}$ and $\mathrm{Up}$ are among $a,b,f,z$ and the parameters, and those of $\varepsilon$ among $a,b,f$ and the parameters.

Let sets $a$, $b$, $f$ and $z$ be assigned to $x_{0},\dots,x_{3}$. If $a,b\in\mathbb{R}$ and $a<b$, then $[a,b]$ has a partition: $\{a,b\}=\{a\}\cup\{b\}$ is finite by Finite Sets: the Pigeonhole Principle, Uniqueness of the Length, Subsets, Unions, Products, Images, Bounded Sets of Natural Numbers, Extreme Elements, Sets of Maps, Finite Unions and Finite Choice (iii) and Finite Sets: the Pigeonhole Principle, Uniqueness of the Length, Subsets, Unions, Products, Images, Bounded Sets of Natural Numbers, Extreme Elements, Sets of Maps, Finite Unions and Finite Choice (v), contains $a$ and $b$, and is a subset of $[a,b]$ by Intervals of the Real Line (ii), as $a\le a\le b$ and $a\le b\le b$, so it is a partition of $[a,b]$ by Partitions of a Closed Interval, the Set of Partitions, and Refinements (i). Therefore $\exists P\,\exists s\,\psi_{L}(a,b,f,P,s)$ holds if and only if $a,b\in\mathbb{R}$, $a<b$ and $f$ is a bounded map $f:[a,b]\to\mathbb{R}$. In that case the remaining conjuncts of $\mathrm{Lo}$ say that $z\in\mathbb{R}$, that $L(f,R)\le z$ for every partition $R$ of $[a,b]$, and that $z\le c$ for every $c\in\mathbb{R}$ with $L(f,R)\le c$ for every partition $R$ of $[a,b]$. By Bounds for Darboux Sums, Monotonicity under Refinement, the Supremum of the Lower Sums and the Infimum of the Upper Sums, and Concatenation of Partitions (iv) exactly one real number has these properties, its number $\lambda_{*}$, and by The Riemann Integral on a Closed Interval via Lower and Upper Integrals (iii) this number is the lower integral of $f$ over $[a,b]$. So $\mathrm{Lo}$ holds if and only if $a,b\in\mathbb{R}$, $a<b$, $f$ is a bounded map $f:[a,b]\to\mathbb{R}$ and $z$ is its lower integral; in the same way, with the number $\lambda^{*}$ of Bounds for Darboux Sums, Monotonicity under Refinement, the Supremum of the Lower Sums and the Infimum of the Upper Sums, and Concatenation of Partitions (iv), $\mathrm{Up}$ holds if and only if the same holds with the upper integral. Hence $\varepsilon$ holds if and only if $a,b\in\mathbb{R}$, $a<b$, $f$ is a bounded map $f:[a,b]\to\mathbb{R}$, and

$$\underline{\int_{a}^{b}}f=\overline{\int_{a}^{b}}f .$$

By The Riemann Integral on a Closed Interval via Lower and Upper Integrals (iv) the last equation says that $f$ is integrable on $[a,b]$. So $\varepsilon$ is a predicative formula in $x_{0},x_{1},x_{2}$ expressing the condition of (i) with $a=x_{0}$, $b=x_{1}$ and $f=x_{2}$. By Renaming and Substituting Variables in Predicative Formulas (i), with its number of variables equal to $3$, its $n$ equal to $N$ and $\sigma(0)=i$, $\sigma(1)=j$, $\sigma(2)=k$, the formula $\varepsilon(x_{i},x_{j},x_{k})$ is a predicative formula in $x_{0},\dots,x_{N-1}$ expressing this condition with $a=x_{i}$, $b=x_{j}$ and $f=x_{k}$. This proves (i).

Integrability on a subinterval. In this paragraph $E$, $g$, $u$, $v$, $h$, $p$, $t$ and $w$ denote $x_{0},\dots,x_{7}$, and $\varepsilon(u,v,h)$ is $\varepsilon(x_{2},x_{3},x_{4})$, which holds exactly when $\varepsilon$ holds with the sets assigned to $u$, $v$ and $h$ assigned to $x_{0}$, $x_{1}$ and $x_{2}$. Let

$$\theta:\quad\forall p\,\Bigl(p\in h\Leftrightarrow\bigl(p\in g\wedge\exists t\,\exists w\,(p=(t,w)\wedge u\le t\wedge t\le v)\bigr)\Bigr),$$ $$\kappa:\quad\forall t\,(t\in E\Rightarrow t\in\mathbb{R})\wedge\mu(g,E,\mathbb{R})\wedge u\in\mathbb{R}\wedge v\in\mathbb{R}\wedge u<v\wedge\forall t\,\bigl((t\in\mathbb{R}\wedge u\le t\wedge t\le v)\Rightarrow t\in E\bigr),$$

and

$$\beta=\kappa\wedge\exists h\,\bigl(\theta\wedge\varepsilon(u,v,h)\bigr).$$

These formulas are predicative, and the free variables of $\beta$ are among $E,g,u,v$ and the parameters.

Let sets $E$, $g$, $u$ and $v$ be assigned to $x_{0},\dots,x_{3}$. By Intervals of the Real Line (ii), $\kappa$ holds if and only if $E\subseteq\mathbb{R}$, $g$ is a map $g:E\to\mathbb{R}$, $u,v\in\mathbb{R}$, $u<v$ and $[u,v]\subseteq E$; if $\kappa$ fails, both $\beta$ and the condition of (ii) fail. Suppose that $\kappa$ holds. For a set $h$, $\theta$ holds if and only if $h=g|_{[u,v]}$: by The Restriction of a Function or Relation to a Class (i) the elements of $g|_{[u,v]}$ are the pairs $(t,w)\in g$ with $t\in[u,v]$; the first component of every pair in $g$ lies in $E\subseteq\mathbb{R}$, so for such a pair $t\in[u,v]$ if and only if $u\le t$ and $t\le v$; and two sets with the same elements are equal (Class Theory NBG: the Axioms, Standing Conventions and Basic Notation (ii)). Hence the formula $\exists h\,(\theta\wedge\varepsilon(u,v,h))$ holds if and only if $\varepsilon$ holds with $u$, $v$ and $g|_{[u,v]}$ assigned to $x_{0}$, $x_{1}$ and $x_{2}$, that is, by the meaning of $\varepsilon$ shown above, if and only if the restriction $g|_{[u,v]}:[u,v]\to\mathbb{R}$ is bounded and integrable on $[u,v]$. By The Riemann Integral on a Closed Interval via Lower and Upper Integrals (vi) this says that $g$ is integrable on $[u,v]$. So $\beta$ is a predicative formula in $x_{0},\dots,x_{3}$ expressing the condition of (ii) with $E=x_{0}$, $g=x_{1}$, $u=x_{2}$ and $v=x_{3}$. By Renaming and Substituting Variables in Predicative Formulas (i), with its number of variables equal to $4$, its $n$ equal to $N$ and $\sigma(0)=i$, $\sigma(1)=j$, $\sigma(2)=k$, $\sigma(3)=l$, the formula $\beta(x_{i},x_{j},x_{k},x_{l})$ is a predicative formula in $x_{0},\dots,x_{N-1}$ expressing this condition with $E=x_{i}$, $g=x_{j}$, $u=x_{k}$ and $v=x_{l}$. This proves (ii).

Defined integrals. In this paragraph $E$, $g$, $u$, $v$ and $t$ denote $x_{0},\dots,x_{4}$, and $\beta(E,g,v,u)$ is $\beta(x_{0},x_{1},x_{3},x_{2})$, which holds exactly when $\beta$ holds with the sets assigned to $E$, $g$, $v$ and $u$ assigned to $x_{0}$, $x_{1}$, $x_{2}$ and $x_{3}$. Let

$$\delta=\forall t\,(t\in E\Rightarrow t\in\mathbb{R})\wedge\mu(g,E,\mathbb{R})\wedge u\in E\wedge v\in E\wedge\bigl(u=v\vee\beta\vee\beta(E,g,v,u)\bigr).$$

It is predicative, with free variables among $E,g,u,v$ and the parameters.

Let sets $E$, $g$, $u$ and $v$ be assigned to $x_{0},\dots,x_{3}$. If $E\not\subseteq\mathbb{R}$, or $g$ is not a map $g:E\to\mathbb{R}$, or $u\notin E$, or $v\notin E$, both $\delta$ and the condition of (iii) fail. Otherwise $u,v\in\mathbb{R}$, and by the meaning of $\beta$ shown above, $\beta$ holds if and only if $u<v$, $[u,v]\subseteq E$ and $g$ is integrable on $[u,v]$, and $\beta(E,g,v,u)$ holds if and only if $v<u$, $[v,u]\subseteq E$ and $g$ is integrable on $[v,u]$, in the sense of The Riemann Integral on a Closed Interval via Lower and Upper Integrals (vi). So $\delta$ holds if and only if $u=v$, or one of these two conditions holds, which by The Riemann Integral on a Closed Interval via Lower and Upper Integrals (viii) says that $\int_{u}^{v}g$ is defined. So $\delta$ is a predicative formula in $x_{0},\dots,x_{3}$ expressing the condition of (iii) with $E=x_{0}$, $g=x_{1}$, $u=x_{2}$ and $v=x_{3}$. By Renaming and Substituting Variables in Predicative Formulas (i), with its number of variables equal to $4$, its $n$ equal to $N$ and $\sigma(0)=i$, $\sigma(1)=j$, $\sigma(2)=k$, $\sigma(3)=l$, the formula $\delta(x_{i},x_{j},x_{k},x_{l})$ is a predicative formula in $x_{0},\dots,x_{N-1}$ expressing this condition with $E=x_{i}$, $g=x_{j}$, $u=x_{k}$ and $v=x_{l}$. This proves (iii).