Toolkit for CA1b

In the setting of Complex Analysis: Standing Notation and The Real Line: Standing Notation and Background for Calculus on Intervals, let real numbers be the elements of the type $\mathrm{Real}$ of The Real Numbers as a Type (i), with $0$, $1$, $+$, $\cdot$, $-$, $\le$ and $<$ as in The Real Numbers as a Type (ii), powers as in The Real Numbers as a Type (iii) and the reciprocal $h^{-1}$ of $h\neq0$ as in The Real Numbers as a Type (vii); the set of $x\in\mathrm{Real}$ is written $\underline{x}$. An element $x$ of $\mathrm{Real}$ stands for the real number $\underline{x}$ wherever a set is needed: in pairs, as an argument of the map $\iota$ below or of a map on $\mathbb{R}$, and as a value of a map into $\mathbb{R}$; so a function $G$ from $\mathrm{Real}$ to $\mathrm{Real}$ stands for the map $\mathbb{R}\to\mathbb{R}$, $\underline{x}\mapsto\underline{G(x)}$; conversely, every real number $s\in\mathbb{R}$ is $\underline{x}$ for exactly one $x\in\mathrm{Real}$ (The Real Numbers as a Type (i)), and the order and operations of $\mathrm{Real}$ correspond to those of $\mathbb{R}$ (The Real Numbers as a Type (ii)), so an order relation or an equation between elements of $\mathrm{Real}$ and real numbers is read through this correspondence. Departing from The Complex Numbers, with the Real Numbers Identified with a Subset of the Complex Numbers (iii), this item handles complex numbers as pairs, as in The Complex Numbers: Pairs of Real Numbers with Their Addition and Multiplication, and the Imaginary Unit: $\mathbb{C}$ is the set of complex numbers $z=(a,b)$ with $a,b\in\mathrm{Real}$, and $\operatorname{re}z=a$, $\operatorname{im}z=b$; the sum and product are those of The Complex Numbers: Pairs of Real Numbers with Their Addition and Multiplication, and the Imaginary Unit (iii), $i$ is the imaginary unit, the zero $0=(0,0)$, negatives and reciprocals are as in The Complex Numbers: Pairs of Real Numbers with Their Addition and Multiplication, and the Imaginary Unit (v), and $\iota(a)=(a,0)$ is the map of The Complex Numbers: Pairs of Real Numbers with Their Addition and Multiplication, and the Imaginary Unit (vi). On a complex number taken as a set, $\operatorname{Re}$ and $\operatorname{Im}$ are the real and imaginary parts and $\overline{u}$ is the complex conjugate. Let $\cos$ be the cosine. For $t\in\mathbb{R}$ and $k\in\mathbb{N}$ let

$$c_{k}(t)=\frac{(-1)^{k-1}t^{2k-2}}{(2k-2)!},\qquad \sigma_{k}(t)=\frac{(-1)^{k-1}t^{2k-1}}{(2k-1)!}$$

formed with the operations of $\mathbb{R}$, with $k-1$, $2k-2$ and $2k-1$ the differences in $\mathbb{N}_{0}$, $t^{n}$ the power ($t^{0}=1$), and the factorials read in $\mathbb{R}$ through their images. In the last two clauses, $F$ and $F'$ are functions from $\mathrm{Real}$ to $\mathrm{Real}$ such that $F$ is differentiable on the interval $\mathbb{R}$ (Basic Facts about Intervals of the Real Line (i)) and $F'$ is its derivative.

(i) Equal squares. For $x,y\in\mathrm{Real}$ with $0\le x$, $0\le y$ and $x\cdot x=y\cdot y$: $x=y$.

(ii) Parts of $a+ib$. For $a,b\in\mathrm{Real}$:

$$\operatorname{re}\bigl(\iota(a)+i\cdot\iota(b)\bigr)=a,\qquad \operatorname{im}\bigl(\iota(a)+i\cdot\iota(b)\bigr)=b.$$

(iii) Parts of $it$. For $t\in\mathrm{Real}$: $\operatorname{re}(i\cdot\iota(t))=0$ and $\operatorname{im}(i\cdot\iota(t))=t$.

(iv) Decomposition. For $z\in\mathbb{C}$: $z=\iota(\operatorname{re}z)+i\cdot\iota(\operatorname{im}z)$.

(v) The conjugate. For $z\in\mathbb{C}$, as sets: $\overline{z}=\iota(\operatorname{re}z)-\iota(\operatorname{im}z)\cdot i$.

(vi) The conjugate of $a+ib$. For $a,b\in\mathrm{Real}$, as sets: $\overline{\iota(a)+i\cdot\iota(b)}=\iota(a)+i\cdot\iota(-b)$.

(vii) Negatives. For $x\in\mathrm{Real}$: $i\cdot\iota(-x)=-(i\cdot\iota(x))$.

(viii) Zero. $i\cdot\iota(0)=0$.

(ix) Membership. Every $z\in\mathbb{C}$, taken as a set, lies in the set $\mathbb{C}$ of The Complex Numbers: Pairs of Real Numbers with Their Addition and Multiplication, and the Imaginary Unit (i).

(x) Parts. For $z\in\mathbb{C}$: $\operatorname{Re}z=\underline{\operatorname{re}z}$ and $\operatorname{Im}z=\underline{\operatorname{im}z}$.

(xi) Squares. For $a\in\mathrm{Real}$: $\underline{a^{2}}=\underline{a}^{2}$, where on the right $\underline{a}^{2}$ is the power for the multiplication of $\mathbb{R}$, with exponent the digit $2$.

(xii) Division by a real number. For $v\in\mathbb{C}$ and $h\in\mathrm{Real}$ with $h\neq0$ and $\iota(h)\neq0$:

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

(xiii) The series terms are real. For $t\in\mathrm{Real}$ and $k\in\mathbb{N}$: $c_{k}(t)\in\mathbb{R}$ and $\sigma_{k}(t)\in\mathbb{R}$.

(xiv) The series terms are predicative. For $t\in\mathrm{Real}$, the condition on distinct set variables $x_{0},x_{1}$ that $x_{0}=k$ for some $k\in\mathbb{N}$ and $x_{1}=c_{k}(t)$ is expressed by a predicative formula, and likewise with $\sigma_{k}(t)$ in place of $c_{k}(t)$, with $x_{0},x_{1}$ in place of the variables of Conditions Expressed by a Predicative Formula, and Guards (i), with no displayed variables, and with the parameters $t$; the sets $\mathbb{N}$, $\mathbb{N}_{0}$ and $\mathbb{R}$; the order, addition, multiplication, $0$ and $1$ of $\mathbb{N}_{0}$ and of $\mathbb{R}$; the elements $2$ of $\mathbb{N}_{0}$ and $-1$ of $\mathbb{R}$; the map $p:\mathbb{R}\times\mathbb{N}_{0}\to\mathbb{R}$, $p(x,m)=x^{m}$, of Powers with a Variable Base: a Predicative Formula and the Map (x, m) ↦ x^m (ii) for the multiplication of $\mathbb{R}$; the map $\Phi:\mathbb{N}_{0}\to\mathbb{N}_{0}$, $\Phi(n)=n!$, of The Factorial as a Map on the Natural Numbers with Zero (i); and the constant map $u:\mathbb{N}_{0}\to\mathbb{R}$ with value $1$.

(xv) Pairing terms of a sum. Let $r$, with $+$, $\cdot$, $0$ and $1$, be a commutative ring, and let $a$ and $b$ be sequences in $r$ with $b_{k}=a_{2k-1}+a_{2k}$ for every $k\in\mathbb{N}$. Then for every $m\in\mathbb{N}$, with the sums over intervals,

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

(xvi) Even terms. Let $X$ be a set and let $a$ and $b$ be sequences in $X$ with $b_{m}=a_{2m}$ for every $m\in\mathbb{N}$. Then $b$ is a subsequence of $a$.

(xvii) The cosine is at most one. For every $t\in\mathrm{Real}$: $\cos t\le1$.

(xviii) Nondecreasing on a ray. If $0\le F'(t)$ for every $t\in\mathrm{Real}$ with $t\ge0$, then $F(s)\le F(t)$ for all $s,t\in\mathrm{Real}$ with $0\le s\le t$.

(xix) Strictly increasing on a closed interval. Let $a,b\in\mathrm{Real}$ with $a<b$. If $0<F'(t)$ for every $t\in\mathrm{Real}$ with $a<t<b$, then $F(s)<F(t)$ for all $s,t\in\mathrm{Real}$ with $a\le s<t\le b$.