Proof of Toolkit for CA1b

Routine facts about typed real numbers, maps, natural numbers and predicativity are used without comment (Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity (vi)).

For (i), let $x,y\in\mathrm{Real}$ with $0\le x$, $0\le y$ and $x\cdot x=y\cdot y$. By the ring laws,

$$(x-y)\cdot(x+y)=x\cdot x-y\cdot y=0,$$

so $x-y=0$ or $x+y=0$, by Rules of Arithmetic and Order in an Ordered Field (i). In the first case $x=y$. In the second case $x=-y$, and $0\le y$ gives $-y\le-0=0$ by Rules of Arithmetic and Order in an Ordered Field (v); hence $0\le x\le0$, so $x=0$, and $y=-x=0=x$.

For (ii), let $a,b\in\mathrm{Real}$. By commutativity of the product of the field $\mathbb{C}$ (The Complex Numbers: Pairs of Real Numbers with Their Addition and Multiplication, and the Imaginary Unit (v)) and the last identity of The Complex Numbers: Pairs of Real Numbers with Their Addition and Multiplication, and the Imaginary Unit (vi),

$$\iota(a)+i\cdot\iota(b)=\iota(a)+\iota(b)\cdot i=(a,b).$$

The entries of the pair $(a,b)$ are $a$ and $b$ (they are determined by the pair, as recorded in The Complex Numbers: Pairs of Real Numbers with Their Addition and Multiplication, and the Imaginary Unit (iii)), so $\operatorname{re}(\iota(a)+i\cdot\iota(b))=a$ and $\operatorname{im}(\iota(a)+i\cdot\iota(b))=b$.

For (iii), let $t\in\mathrm{Real}$. By The Complex Numbers: Pairs of Real Numbers with Their Addition and Multiplication, and the Imaginary Unit (vi), $\iota(0)=(0,0)$, which is the zero of $\mathbb{C}$ (The Complex Numbers: Pairs of Real Numbers with Their Addition and Multiplication, and the Imaginary Unit (v)); hence $i\cdot\iota(t)=\iota(0)+i\cdot\iota(t)$, and (ii) with $a=0$ and $b=t$ gives $\operatorname{re}(i\cdot\iota(t))=0$ and $\operatorname{im}(i\cdot\iota(t))=t$.

For (iv), let $z\in\mathbb{C}$. Then $z=(\operatorname{re}z,\operatorname{im}z)$ by the definition of the entries, and by the last identity of The Complex Numbers: Pairs of Real Numbers with Their Addition and Multiplication, and the Imaginary Unit (vi) and commutativity of the product,

$$z=\iota(\operatorname{re}z)+\iota(\operatorname{im}z)\cdot i=\iota(\operatorname{re}z)+i\cdot\iota(\operatorname{im}z).$$

For (v), let $z\in\mathbb{C}$, $a=\operatorname{re}z$ and $b=\operatorname{im}z$. By The Complex Numbers: Pairs of Real Numbers with Their Addition and Multiplication, and the Imaginary Unit (v), the set $\mathbb{C}$, the sum, the product and $i$ of The Complex Numbers: Pairs of Real Numbers with Their Addition and Multiplication, and the Imaginary Unit are those used here, and by The Earlier and the New Versions of the Definitions of the Natural Numbers, the Complex Numbers, the Conjugate and the Modulus Agree, and the Two Versions of Real Correspond (ii) they are also those of The Complex Numbers: Pairs of Real Numbers with Their Addition and Multiplication, and the Imaginary Unit (i), The Complex Numbers: Pairs of Real Numbers with Their Addition and Multiplication, and the Imaginary Unit (iii) and The Complex Numbers: Pairs of Real Numbers with Their Addition and Multiplication, and the Imaginary Unit (iv); so the negatives and differences of The Complex Numbers, with the Real Numbers Identified with a Subset of the Complex Numbers (ii) are those here, and the map $\iota$ of The Complex Numbers, with the Real Numbers Identified with a Subset of the Complex Numbers (iv), given by $a\mapsto(a,0)$ like the one here, is the same map. By The Complex Conjugate of a Complex Number (i), read through the identification of a real number with its image under $\iota$ (The Complex Numbers, with the Real Numbers Identified with a Subset of the Complex Numbers (v)), $\overline{z}=\iota(\operatorname{Re}z)-\iota(\operatorname{Im}z)\cdot i$. By (x), $\operatorname{Re}z=\underline{a}$ and $\operatorname{Im}z=\underline{b}$, so $\overline{z}=\iota(a)-\iota(b)\cdot i$.

For (vi), let $a,b\in\mathrm{Real}$ and $w=\iota(a)+i\cdot\iota(b)$. By (ii), $\operatorname{re}w=a$ and $\operatorname{im}w=b$, so by (v)

$$\overline{w}=\iota(a)-\iota(b)\cdot i=\iota(a)+(-\iota(b))\cdot i=\iota(a)+i\cdot\iota(-b).$$

The second equality holds because a difference is the sum with the negative and $-(\iota(b)\cdot i)=(-\iota(b))\cdot i$ by the ring laws; the third because $-\iota(b)=\iota(-b)$ by The Complex Numbers: Pairs of Real Numbers with Their Addition and Multiplication, and the Imaginary Unit (vi) and the product of $\mathbb{C}$ is commutative.

For (vii), let $x\in\mathrm{Real}$. By The Complex Numbers: Pairs of Real Numbers with Their Addition and Multiplication, and the Imaginary Unit (vi), $\iota(-x)=-\iota(x)$, and $i\cdot(-u)=-(i\cdot u)$ for every $u\in\mathbb{C}$ by the ring laws; hence $i\cdot\iota(-x)=-(i\cdot\iota(x))$.

For (viii): by The Complex Numbers: Pairs of Real Numbers with Their Addition and Multiplication, and the Imaginary Unit (vi), $\iota(0)=(0,0)$, the zero of $\mathbb{C}$, and $i\cdot0=0$ in the field $\mathbb{C}$; hence $i\cdot\iota(0)=0$.

For (ix), let $z\in\mathbb{C}$. Then $z\in\mathbb{R}\times\mathbb{R}$ by The Complex Numbers: Pairs of Real Numbers with Their Addition and Multiplication, and the Imaginary Unit (i), and by The Complex Numbers: Pairs of Real Numbers with Their Addition and Multiplication, and the Imaginary Unit (v) this is the set $\mathbb{C}$ of The Complex Numbers: Pairs of Real Numbers with Their Addition and Multiplication, and the Imaginary Unit (i).

For (x), let $z\in\mathbb{C}$, $a=\operatorname{re}z$ and $b=\operatorname{im}z$. As in the proof of (iv), $z=\iota(a)+\iota(b)\cdot i$. By The Complex Numbers: Pairs of Real Numbers with Their Addition and Multiplication, and the Imaginary Unit (v), this is the set, sum, product and imaginary unit of The Complex Numbers, with the Real Numbers Identified with a Subset of the Complex Numbers (ii), and the map $\iota$ of The Complex Numbers, with the Real Numbers Identified with a Subset of the Complex Numbers (iv), which is $a\mapsto(a,0)$, is the one used here. Read through The Complex Numbers, with the Real Numbers Identified with a Subset of the Complex Numbers (v), this says $z=\underline{a}+\underline{b}\,i$ with the real numbers $\underline{a}$ and $\underline{b}$. By the uniqueness in The Complex Numbers, with the Real Numbers Identified with a Subset of the Complex Numbers (vii) and by Real and Imaginary Parts of a Complex Number (i), $\operatorname{Re}z=\underline{a}$ and $\operatorname{Im}z=\underline{b}$.

For (xi), let $a\in\mathrm{Real}$. By The Real Numbers as a Type (iii), $a^{2}=a^{1}\cdot a=(a^{0}\cdot a)\cdot a=(1\cdot a)\cdot a$, which is $a\cdot a$ by The Real Numbers as a Type (iv); its set is $\underline{a}\cdot\underline{a}$, the product in $\mathbb{R}$ (The Real Numbers as a Type (ii)). On the other side, $2=1+1$ in $\mathbb{N}_{0}$ by Arithmetic and Order of the Natural Numbers (xiv), so in the commutative ring $\mathbb{R}$

$$\underline{a}^{2}=\underline{a}^{1}\cdot\underline{a}^{1}=\underline{a}\cdot\underline{a}$$

by Powers in a Commutative Ring, a Field and an Ordered Field: Exponent Laws, Factorisation, Geometric Sums, Monotonicity and Bernoulli's Inequality (i) and Powers in a Commutative Ring, a Field and an Ordered Field: Exponent Laws, Factorisation, Geometric Sums, Monotonicity and Bernoulli's Inequality (ii). Hence $\underline{a^{2}}=\underline{a}^{2}$.

For (xii), let $v\in\mathbb{C}$ and $h\in\mathrm{Real}$ with $h\neq0$ and $\iota(h)\neq0$. The set of the reciprocal $h^{-1}$ is the reciprocal of $\underline{h}$ in $\mathbb{R}$ (The Real Numbers as a Type (vii)), so $\iota(h)^{-1}=\iota(h^{-1})$ by The Complex Numbers: Pairs of Real Numbers with Their Addition and Multiplication, and the Imaginary Unit (vi). By (iv), $v=\iota(\operatorname{re}v)+i\cdot\iota(\operatorname{im}v)$. By the ring laws in $\mathbb{C}$ and $\iota(cd)=\iota(c)\cdot\iota(d)$ (The Complex Numbers: Pairs of Real Numbers with Their Addition and Multiplication, and the Imaginary Unit (vi)),

$$v\cdot\iota(h)^{-1}=\iota(\operatorname{re}v)\cdot\iota(h^{-1})+i\cdot\bigl(\iota(\operatorname{im}v)\cdot\iota(h^{-1})\bigr)=\iota(\operatorname{re}v\cdot h^{-1})+i\cdot\iota(\operatorname{im}v\cdot h^{-1}),$$

and (ii) gives $\operatorname{re}(v\cdot\iota(h)^{-1})=\operatorname{re}v\cdot h^{-1}$ and $\operatorname{im}(v\cdot\iota(h)^{-1})=\operatorname{im}v\cdot h^{-1}$.

For (xiii), let $t\in\mathrm{Real}$ and $k\in\mathbb{N}$. Since $1\le k$, $2\le2k$ and $1\le2k$ in $\mathbb{N}_{0}$, the differences $k-1$, $2k-2$ and $2k-1$ exist in $\mathbb{N}_{0}$ (The Difference of Two Natural Numbers with Zero (i)). In the ordered field $\mathbb{R}$, $-1\in\mathbb{R}$ by Closure Facts in an Ordered Field: Negatives, Differences, Quotients, Absolute Values, Powers, Natural Numbers, Halves and Minima (i); the powers $(-1)^{k-1}$, $t^{2k-2}$ and $t^{2k-1}$ lie in $\mathbb{R}$ by Closure Facts in an Ordered Field: Negatives, Differences, Quotients, Absolute Values, Powers, Natural Numbers, Halves and Minima (iv), and so do their products; the factorials $(2k-2)!$ and $(2k-1)!$ read in $\mathbb{R}$ lie in $\mathbb{R}$ by Closure Facts in an Ordered Field: Negatives, Differences, Quotients, Absolute Values, Powers, Natural Numbers, Halves and Minima (v) and are nonzero by Natural Numbers and Factorials Read in the Reals: the Order Carries Over, One Is Least, and Factorials Are Positive, Recursive and Nondecreasing (iii). Hence the quotients $c_{k}(t)$ and $\sigma_{k}(t)$ lie in $\mathbb{R}$ by Closure Facts in an Ordered Field: Negatives, Differences, Quotients, Absolute Values, Powers, Natural Numbers, Halves and Minima (ii).

For (xiv), fix $t\in\mathrm{Real}$; we treat $c_{k}(t)$, the case of $\sigma_{k}(t)$ differing only where noted. Let $p$, $\Phi$ and $u$ be the maps named in (xiv). Consider the formula tree with the two set variables $x_{0},x_{1}$ that is the conjunction of the atom $x_{0}\in\mathbb{N}$ with the tree that names in turn the values

$$\begin{aligned} &x_{2}=x_{0}-1\text{ with }\theta_{2}:\ x_{2}\in\mathbb{N}_{0}\text{ and }x_{2}+1=x_{0},\\ &x_{3}=2\cdot x_{0}\ \text{(in }\mathbb{N}_{0}),\\ &x_{4}=x_{3}-2\text{ with }\theta_{4}:\ x_{4}\in\mathbb{N}_{0}\text{ and }x_{4}+2=x_{3},\\ &x_{5}=p(-1,x_{2}),\\ &x_{6}=p(t,x_{4}),\\ &x_{7}=\Phi(x_{4}),\\ &x_{8}=1\text{ with }\theta_{8}:\ x_{8}=1,\\ &x_{9}=\textstyle\sum_{l=x_{8}}^{x_{7}}u_{l}\text{ with }\theta_{9}:\ x_{8},x_{7}\in\mathbb{N}_{0}\text{ and }x_{9}=\textstyle\sum_{l=x_{8}}^{x_{7}}u_{l},\\ &x_{10}=x_{5}\cdot x_{6}\ \text{(in }\mathbb{R}), \end{aligned}$$

and then has the atom of its own "$x_{10},x_{9}\in\mathbb{R}$, $x_{9}\neq0$ and $x_{1}=x_{10}/x_{9}$"; here the classes $\tau$ of the values named with a condition are the differences $x_{0}-1$ and $x_{3}-2$ in $\mathbb{N}_{0}$, the parameter $1$, and the sum over the interval from $x_{8}$ to $x_{7}$. For $\sigma_{k}(t)$, the value $x_{4}$ is named as $x_{3}-1$ with $\theta_{4}$ reading "$x_{4}\in\mathbb{N}_{0}$ and $x_{4}+1=x_{3}$". Here $x_{3}$, $x_{5}$, $x_{6}$ and $x_{10}$ are named values of the form $v\ast w$, with $\ast$ the multiplication of $\mathbb{N}_{0}$, $p$, $p$ and the multiplication of $\mathbb{R}$, and $x_{7}$ is a named value $\Phi(v)$. The tree is well scoped, as each named variable is new and is used only after it is named. Its side conditions hold: the parameters $1$, $2$, $-1$ and $t$ standing as arguments are sets; $\theta_{2}$, $\theta_{4}$ and $\theta_{8}$ are memberships and equalities with values of the addition of $\mathbb{N}_{0}$, which are predicative (Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity (v)); $\theta_{9}$ is predicative by Predicative Formulas for the Vocabulary of Finite Combinatorics, at Any Variable Positions (vi), applied to the sum of $\mathbb{R}$, which is associative and commutative with neutral element $0$ (Commutative Rings (i)); and the final atom is predicative by Predicative Formulas for Differences, Quotients, Absolute Values, Distances and the Strict Order of the Real Numbers, at Any Variable Positions (ii). The tree uses its values properly under every assignment: the named part is read only where $x_{0}=k\in\mathbb{N}$, and there $x_{2}=k-1$ and $x_{4}=2k-2$ (respectively $2k-1$) exist and are unique by The Difference of Two Natural Numbers with Zero (i), the pairs $(2,k)$, $(-1,k-1)$ and $(t,2k-2)$ and the number $2k-2$ lie in the domains of the multiplication of $\mathbb{N}_{0}$, of $p$ and of $\Phi$, $x_{8}=1$ is unique, $x_{9}$ is a uniquely determined element of $\mathbb{R}$, and $x_{5},x_{6}\in\mathbb{R}$. By The Graph Reading of a Formula Tree Is Predicative and Agrees with Its Reading, So the Reading Is Predicative (iii), the reading of the tree is the reading of a predicative formula whose free variables are among $x_{0},x_{1}$ and class variables standing for parameters; each parameter of the tree, of its conditions $\theta$ and of its atom of its own is one of those listed in (xiv). That reading fails where $x_{0}\notin\mathbb{N}$, as does the condition, which requires $x_{0}=k$ for some $k\in\mathbb{N}$. Where $x_{0}=k\in\mathbb{N}$, the named values are $k-1$, $2k$, $2k-2$, $(-1)^{k-1}$, $t^{2k-2}$, $(2k-2)!$, $1$, the image of $(2k-2)!$ in $\mathbb{R}$ (by The Image of a Natural Number in a Commutative Ring (i), Sums and Products over a Finite Set and over an Interval (iv) and Sums and Products over a Finite Set and over an Interval (ii)), and $(-1)^{k-1}t^{2k-2}$; this image is nonzero by Natural Numbers and Factorials Read in the Reals: the Order Carries Over, One Is Least, and Factorials Are Positive, Recursive and Nondecreasing (iii), so the reading holds exactly when $x_{1}=c_{k}(t)$. Hence that formula expresses the condition, in the sense of Conditions Expressed by a Predicative Formula, and Guards (ii).

For (xv), the sum of $r$ is associative and commutative with neutral element $0$ (Commutative Rings (i)), so the sums over intervals are defined (Sums and Products over a Finite Set and over an Interval (iv)). We argue by induction on $m\in\mathbb{N}$ (the condition on $m$ is predicative by Predicative Formulas for the Vocabulary of Finite Combinatorics, at Any Variable Positions (vi), with $2m$ a value of the multiplication of $\mathbb{N}_{0}$, predicative by The Graph of Multiplication on ℕ₀ Is Given by a Predicative Formula (i)). For $m=1$, Iterated Operations over Finite Sets: Singletons, Disjoint Unions, Reindexing, Products of Sets, Termwise Combination, Homomorphisms and Intervals (vii) and Iterated Operations over Finite Sets: Singletons, Disjoint Unions, Reindexing, Products of Sets, Termwise Combination, Homomorphisms and Intervals (i) give

$$\sum_{n=1}^{2}a_{n}=\sum_{n=1}^{1}a_{n}+a_{2}=a_{1}+a_{2}=b_{1}=\sum_{k=1}^{1}b_{k}.$$

Suppose the identity holds for $m$. In $\mathbb{N}$, $2(m+1)=2m+2=(2m+1)+1$ and $2(m+1)-1=2m+1$, so the hypothesis on $b$ at $k=m+1$ reads $b_{m+1}=a_{2m+1}+a_{2m+2}$. Hence

$$\sum_{n=1}^{2(m+1)}a_{n}=\Bigl(\sum_{n=1}^{2m}a_{n}+a_{2m+1}\Bigr)+a_{2m+2}=\sum_{k=1}^{m}b_{k}+\bigl(a_{2m+1}+a_{2m+2}\bigr)=\sum_{k=1}^{m}b_{k}+b_{m+1}=\sum_{k=1}^{m+1}b_{k}:$$

the first equality is Iterated Operations over Finite Sets: Singletons, Disjoint Unions, Reindexing, Products of Sets, Termwise Combination, Homomorphisms and Intervals (vii) applied twice, the second is the induction hypothesis together with associativity of $+$, the third is the hypothesis on $b$ at $k=m+1$, and the last is Iterated Operations over Finite Sets: Singletons, Disjoint Unions, Reindexing, Products of Sets, Termwise Combination, Homomorphisms and Intervals (vii) once more.

For (xvi), let $\tau:\mathbb{N}\to\mathbb{N}$, $\tau(m)=2m$; it maps into $\mathbb{N}$ as $2m\ge1$. Since $\tau(m)=2m<2m+2=\tau(m+1)$ for every $m\in\mathbb{N}$, $\tau$ is strictly increasing. The maps $a\circ\tau$ and $b$ from $\mathbb{N}$ to $X$ satisfy $(a\circ\tau)(m)=a_{2m}=b_{m}$ for every $m\in\mathbb{N}$, so $b=a\circ\tau$, which is a subsequence of $a$ by Subsequences (i).

For (xvii), let $t\in\mathrm{Real}$. Then $\cos t\in\mathbb{R}$ (The Real Sine and Cosine Functions (i)) and $|\cos t|\le1$ by The Pythagorean Identity for Sine and Cosine (ii); read in $\mathrm{Real}$ for the element $\cos t$, whose set is this real number, this gives $-1\le\cos t$ and $\cos t\le1$ (Differences, Quotients and Absolute Values of Real Numbers, and Their Order in the Extended Real Line, Read in the Type Real (iv)).

For (xviii), let $J=[0,\infty)$, an interval by Basic Facts about Intervals of the Real Line (vi), containing the two distinct points $0$ and $1$; let $g=F|_{J}$ be the restriction, with derivatives of $g$ taken relative to $J$. Let $x\in J$. Since $F$ is differentiable at $x$ relative to $\mathbb{R}$ (Derivative of a Real Function on an Interval (iii)), it is continuous at $x$ by The Increment Form of the Derivative, and Differentiability Implies Continuity (ii), so $g$ is continuous at $x$ relative to $J$ by Restriction Stability of Continuity and of the Derivative (i); and $g$ is differentiable at $x$ with $g'(x)=F'(x)$ by Restriction Stability of Continuity and of the Derivative (ii). Hence $g$ is continuous on $J$ and differentiable at every inner point of $J$, and every inner point $x$ of $J$ lies in $J$, so $x\ge0$, and the hypothesis, applied to the element of $\mathrm{Real}$ with set $x$, gives $g'(x)=F'(x)\ge0$. By The Sign and Size of the Derivative: Monotonicity, Constancy and Lipschitz Bounds (i), $g(s)\le g(t)$ for all $s,t\in J$ with $s\le t$. If $0\le s\le t$, then $s,t\in J$, and $F(s)=g(s)\le g(t)=F(t)$.

For (xix), let $a<b$ and $J=[a,b]$, an interval containing the two distinct points $a$ and $b$ by Basic Facts about Intervals of the Real Line (v), and let $g=F|_{J}$. Exactly as for (xviii), $g$ is continuous on $J$ and differentiable at every point of $J$ with $g'(x)=F'(x)$, by The Increment Form of the Derivative, and Differentiability Implies Continuity (ii), Restriction Stability of Continuity and of the Derivative (i) and Restriction Stability of Continuity and of the Derivative (ii). If $x$ is an inner point of $J$, say $u<x<v$ with $u,v\in J$, then $a\le u<x<v\le b$, so $a<x<b$, and the hypothesis, applied to the element of $\mathrm{Real}$ with set $x$, gives $g'(x)=F'(x)>0$. By The Sign and Size of the Derivative: Monotonicity, Constancy and Lipschitz Bounds (ii), $g(s)<g(t)$ for all $s,t\in J$ with $s<t$. If $a\le s<t\le b$, then $s,t\in J$, and $F(s)=g(s)<g(t)=F(t)$.