Proof of Kit for def:complex-exponential

Routine facts about sets, natural numbers, maps and predicative formulas are used without comment (Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity): the values of the parameters are sets ($\le$ and $<$ are subclasses of $\mathbb{R}\times\mathbb{R}$, hence sets by Subclasses of Sets Are Sets, the Union and Power Set of a Set Exist Uniquely, Binary Unions of Sets Are Sets, and the Universal Class Is Proper (i), and the maps among the parameters are sets as elements of the corresponding class of functions by The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (i), products such as $\mathbb{C}\times\mathbb{C}$ and $\mathbb{R}\times\mathbb{R}$ being sets by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set (ii)), elements of classes are sets (Classes, Membership, Sets and Proper Classes (i)), and the one-entry tuple $\langle a\rangle$ is $a$ (The Ordered Pair of Two Sets and Nested Tuples (ii)). The parameters are those of the statement, at their fixed values as in Conditions Expressed by a Predicative Formula, and Guards (i); in formulas, $u_{1}$ denotes the element $1$ of $\mathbb{N}$, $\beta$ the addition of $\mathbb{N}_{0}$, $\oplus$ and $\odot$ the sum and product operations of $\mathbb{C}$, and $o$ the unit of $\mathbb{C}$. In $\mathbb{C}$, which is a field, in particular a commutative ring, by The Complex Numbers, with the Real Numbers Identified with a Subset of the Complex Numbers (ii), an element of $\mathbb{N}_{0}$ denotes its image, as in Commutative Rings, Fields and Ordered Fields: Standard Notation (iv). We write $F,z,w,t,s,c$ for the distinct set variables $x_{0},\dots,x_{5}$ of Renaming and Substituting Variables in Predicative Formulas, the given $x_{0},\dots,x_{n-1}$ being the first of the variables $x_{0},x_{1},\dots$ there; we build a predicative formula in $F$ alone and move it to the position $i$ at the end. The letters $r,q,a,b,y,g$ denote further pairwise distinct set variables, distinct from $x_{0},\dots,x_{5}$. The parameters are set variables other than $x_{0},\dots,x_{n-1}$, other than $x_{0},\dots,x_{5}$, and other than the letters $r,q,a,b,y,g$ and all other bound variables used below.

Sequences in $\mathbb{C}$. Kit for def:sequence-nbg (i), for two variables and the positions $0$ and $1$, gives a predicative formula in $x_{0},x_{1}$ expressing that $x_{0}$ is a sequence in $x_{1}$. For $m\le5$, Renaming and Substituting Variables in Predicative Formulas (iii) with $\tau_{0}=x_{m}$ and $\tau_{1}=\mathbb{C}$ turns it into a predicative formula $\eta(x_{m})$ in $x_{0},\dots,x_{5}$ that holds exactly when $x_{m}$ is a sequence in $\mathbb{C}$, that is, a map $\mathbb{N}\to\mathbb{C}$. Every sequence in $\mathbb{C}$, a map between sets, is a set.

Reading rules. (a) For a map $h:\mathbb{N}\to\mathbb{C}$ and all sets $r$ and $u$: $(r,u)\in h$ if and only if $r\in\mathbb{N}$ and $u=h(r)$, by Maps between Classes: Values, Pairs, Extensionality, Restrictions, Constant Maps and Preimages (ii). (b) For $r\in\mathbb{N}$ and every set $q$: $((r,u_{1}),q)\in\beta$ if and only if $q=r+1$; and for $u,v\in\mathbb{C}$ and every set $y$: $((u,v),y)\in{\oplus}$ if and only if $y=u+v$, and $((u,v),y)\in{\odot}$ if and only if $y=uv$. These are Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (xi), for the binary operation $+$ on $\mathbb{N}_{0}$ (The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion (iv)), with $\mathbb{N}\subseteq\mathbb{N}_{0}$, and for the binary operations of $\mathbb{C}$ (The Complex Numbers: Pairs of Real Numbers with Their Addition and Multiplication, and the Imaginary Unit (iii)). (c) By 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 (iv), each formula of the form $(\cdot,\cdot)\in\cdot$ or $((\cdot,\cdot),\cdot)\in\cdot$ written below is predicative and, when sets are assigned to the variables inside the pairs, holds if and only if the corresponding membership of ordered pairs holds; the values of $u_{1}$ and $o$ are sets, as noted at the start. Each formula below is built from such formulas and from formulas already shown predicative by connectives and quantifiers over set variables, with abbreviations as in Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations (vi); so it is predicative by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (i).

Sequences fixed by a recursion. Let $h,h':\mathbb{N}\to\mathbb{C}$ be maps with $h(1)=h'(1)$ such that, for every $r\in\mathbb{N}$, $h(r)=h'(r)$ implies $h(r+1)=h'(r+1)$. Then $h=h'$. Indeed, apply Composite Maps into Classes, Images of Singletons, and Agreement of Maps by Induction (iii) with $\mathbb{N}$ as its classes $A$, $B$ and $T$, $\mathbb{C}$ as its $X$ and $Y$, and $h$ and $h'$ as its maps $S$ and $M$. Its first hypothesis holds vacuously, as $0\notin\mathbb{N}$. For its second, let $k\in\mathbb{N}_{0}$ with $h(k)=h'(k)$ if $k\in\mathbb{N}$: if $k=0$, then $k+1=1$ and $h(1)=h'(1)$; otherwise $k\in\mathbb{N}$ and $h(k+1)=h'(k+1)$ by assumption. So $h(k)=h'(k)$ for every $k\in\mathbb{N}$, and $h=h'$ by Maps between Classes: Values, Pairs, Extensionality, Restrictions, Constant Maps and Preimages (iii).

The natural numbers in $\mathbb{C}$. Let

$$\nu(c)=\eta(c)\wedge(u_{1},o)\in c\wedge\forall r\,\forall q\,\forall a\,\forall b\,\bigl(((r,a)\in c\wedge((r,u_{1}),q)\in\beta\wedge((a,o),b)\in{\oplus})\Rightarrow(q,b)\in c\bigr).$$

Assign to $c$ a sequence in $\mathbb{C}$. By (a), $(u_{1},o)\in c$ says $c(1)=1$. By (a) and (b), the premises of the implication say that $r\in\mathbb{N}$, $a=c(r)$, $q=r+1$ and $b=c(r)+1$, and by (a) its conclusion then says $c(r+1)=b$; since such $a$, $q$ and $b$ exist for every $r\in\mathbb{N}$, the last conjunct reads $c(r+1)=c(r)+1$ for every $r\in\mathbb{N}$. Now Maps Given by Iterated Operations: Partial Iterates, Images of Natural Numbers, Powers and Operations over a Finite Set (ii) gives a map $\mathbb{N}_{0}\to\mathbb{C}$, $k\mapsto k$, and its restriction $N$ to $\mathbb{N}$ is a sequence in $\mathbb{C}$ with $N(k)=k$ for every $k\in\mathbb{N}$ (Maps between Classes: Values, Pairs, Extensionality, Restrictions, Constant Maps and Preimages (vi)). In $\mathbb{C}$, $N(1)=1$ and $N(r+1)=r+1=N(r)+1$, by The Image of the Natural Numbers with Zero in a Commutative Ring Respects Zero, One, Sums, Products, Differences, Powers, and Finite Sums and Products (i) and The Image of the Natural Numbers with Zero in a Commutative Ring Respects Zero, One, Sums, Products, Differences, Powers, and Finite Sums and Products (ii); so $\nu(N)$ holds. Conversely, if $\nu(c)$ holds, then $c(1)=1=N(1)$, and $c(r)=N(r)$ gives $c(r+1)=c(r)+1=N(r)+1=N(r+1)$; so $c=N$ by the recursion paragraph. Hence $N$, a set as a sequence in $\mathbb{C}$, is the only set $c$ with $\nu(c)$.

The terms. For $z\in\mathbb{C}$ let $T_{z}$ be the sequence of The Complex Exponential Series Converges Absolutely, and Its Sum Is a Function on ℂ (i), with $T_{z}(k)=z^{k-1}/(k-1)!$ for every $k\in\mathbb{N}$. Let

$$\theta(z,t)=z\in\mathbb{C}\wedge\eta(t)\wedge(u_{1},o)\in t\wedge\exists c\,\bigl(\nu(c)\wedge\forall r\,\forall q\,\forall a\,\forall b\,\forall y\,\forall g\,(\chi\Rightarrow((a,z),g)\in{\odot})\bigr),$$ $$\chi=(r,a)\in t\wedge((r,u_{1}),q)\in\beta\wedge(q,b)\in t\wedge(r,y)\in c\wedge((b,y),g)\in{\odot}.$$

Assign sets to $z$ and $t$, with $z\in\mathbb{C}$ and $t$ a sequence in $\mathbb{C}$. As $N$ is the only set with $\nu$, the existential conjunct holds if and only if its implication holds with $c$ assigned $N$. Then, by (a) and (b), $\chi$ says that $r\in\mathbb{N}$, $a=t(r)$, $q=r+1$, $b=t(r+1)$, $y=N(r)=r$ and $g=t(r+1)\,r$, and the conclusion says $g=t(r)\,z$, by (b). Hence $\theta(z,t)$ holds if and only if $z\in\mathbb{C}$, $t$ is a sequence in $\mathbb{C}$, $t(1)=1$ and

$$t(r+1)\,r=t(r)\,z\qquad\text{for every }r\in\mathbb{N}.$$

The sequence $T_{z}$ has these properties. First, $T_{z}(1)=z^{0}/0!=1$, as $z^{0}=1$ (Commutative Rings, Fields and Ordered Fields: Standard Notation (iii)) and $0!=1$ (The Factorial: Recursion, Positivity and Bounds by Powers (i)). Next let $r\in\mathbb{N}$, so that $(r+1)-1=r$ and $r=(r-1)+1$ in $\mathbb{N}_{0}$. Then $z^{r}=z^{r-1}z$ 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), and $r!=r\,(r-1)!$ by The Factorial: Recursion, Positivity and Bounds by Powers (i), also in $\mathbb{C}$ by Commutative Rings, Fields and Ordered Fields: Standard Notation (iv). Moreover $r\neq0$ and $(r-1)!\neq0$ in $\mathbb{C}$: both are at least $1$ in $\mathbb{N}_{0}$, the second by The Factorial: Recursion, Positivity and Bounds by Powers (ii), and equality of elements of $\mathbb{N}_{0}$ is the same in $\mathbb{C}$, by The Complex Numbers, with the Real Numbers Identified with a Subset of the Complex Numbers (vi). Hence

$$T_{z}(r+1)\,r=\frac{z^{r}}{r!}\,r=\frac{z^{r-1}\,z\,r}{r\,(r-1)!}=\frac{z^{r-1}}{(r-1)!}\,z=T_{z}(r)\,z.$$

Conversely, let $t$ be a sequence in $\mathbb{C}$ with $t(1)=1$ and $t(r+1)\,r=t(r)\,z$ for every $r\in\mathbb{N}$. Then $t(1)=T_{z}(1)$, and if $t(r)=T_{z}(r)$, then $t(r+1)\,r=T_{z}(r)\,z=T_{z}(r+1)\,r$, so $t(r+1)=T_{z}(r+1)$, as $r\neq0$; hence $t=T_{z}$ by the recursion paragraph. So, for all sets $z$ and $t$, $\theta(z,t)$ holds if and only if $z\in\mathbb{C}$ and $t=T_{z}$.

Partial sums. For a sequence $t$ in $\mathbb{C}$, let $P_{t}$ be its sequence of partial sums, $P_{t}(m)=\sum_{k=1}^{m}t(k)$. This sum over $\{1,\dots,m\}$ is the iterated operation of $t$ along $[m]$ (Sums and Products over a Finite Set and over an Interval (iv) and Iterated Operations: Finite Sums and Finite Products (ii)), so $P_{t}$ is a map $\mathbb{N}\to\mathbb{C}$ by Maps Given by Iterated Operations: Partial Iterates, Images of Natural Numbers, Powers and Operations over a Finite Set (i). By Iterated Operations: Recursion, Splitting, Reordering, Termwise Combination and Homomorphisms (i), applied to the restrictions of $t$ to $[1]$ and to $[r+1]$, the latter restricting to $[r]$ as $t$ does (Maps between Classes: Values, Pairs, Extensionality, Restrictions, Constant Maps and Preimages (iv)),

$$P_{t}(1)=t(1)\qquad\text{and}\qquad P_{t}(r+1)=P_{t}(r)+t(r+1)\quad\text{for every }r\in\mathbb{N}.$$

Let

$$\pi(t,s)=\eta(t)\wedge\eta(s)\wedge\exists y\,\bigl((u_{1},y)\in t\wedge(u_{1},y)\in s\bigr)\wedge\forall r\,\forall q\,\forall a\,\forall b\,\forall g\,\bigl(((r,a)\in s\wedge((r,u_{1}),q)\in\beta\wedge(q,b)\in t\wedge((a,b),g)\in{\oplus})\Rightarrow(q,g)\in s\bigr).$$

For sequences $t$ and $s$ in $\mathbb{C}$, the third conjunct says $s(1)=t(1)$, by (a), and, read with (a) and (b) as in the previous paragraphs, the last says $s(r+1)=s(r)+t(r+1)$ for every $r\in\mathbb{N}$. These are the identities displayed for $P_{t}$; and if $s$ satisfies them, then $s(1)=P_{t}(1)$, and $s(r)=P_{t}(r)$ gives $s(r+1)=P_{t}(r)+t(r+1)=P_{t}(r+1)$, so $s=P_{t}$ by the recursion paragraph. Hence, for all sets $t$ and $s$, $\pi(t,s)$ holds if and only if $t$ is a sequence in $\mathbb{C}$ and $s=P_{t}$.

Convergence. Kit for def:convergent-sequence-metric-space (i), for four variables with its $i,j,k,l$ equal to $0,1,2,3$, gives a predicative formula in $x_{0},\dots,x_{3}$ expressing that $(x_{0},x_{1})$ is a metric space, $x_{2}$ is a sequence in $x_{0}$, $x_{3}\in x_{0}$ and $x_{2}$ converges to $x_{3}$ in $(x_{0},x_{1})$; its parameters are among those of the statement. So Renaming and Substituting Variables in Predicative Formulas (iii), with $\tau_{0}=\mathbb{C}$, $\tau_{1}=d_{\mathbb{C}}$, $\tau_{2}=s$ and $\tau_{3}=w$, gives a predicative formula $\kappa(s,w)$ in $x_{0},\dots,x_{5}$ that holds exactly when $(\mathbb{C},d_{\mathbb{C}})$ is a metric space, $s$ is a sequence in $\mathbb{C}$, $w\in\mathbb{C}$ and $s$ converges to $w$ in $(\mathbb{C},d_{\mathbb{C}})$. The first holds by Metric Spaces: Balls, the Metric Topology, and the Real and Complex Numbers as Metric Spaces (v), and for a sequence $s$ in $\mathbb{C}$ and $w\in\mathbb{C}$ the last holds if and only if $s\to w$ in the sense of Convergent Sequences of Complex Numbers (i), by Limits of Complex Sequences: Uniqueness, Real and Imaginary Parts, Arithmetic, Real Sequences, Conjugates, Moduli, the Cauchy Criterion and the Modulus Metric (vii). So $\kappa(s,w)$ holds if and only if $s$ is a sequence in $\mathbb{C}$, $w\in\mathbb{C}$ and $s\to w$.

The exponential. Let $z\in\mathbb{C}$. By The Complex Exponential Series Converges Absolutely, and Its Sum Is a Function on ℂ (ii) the series of $T_{z}$ converges, that is, $P_{T_{z}}$ is convergent (Series of Complex Numbers: Partial Sums, Convergence, the Sum and Absolute Convergence (ii)), and its sum, the limit of $P_{T_{z}}$, is $\exp z$ (The Complex Exponential Function (i)); so $P_{T_{z}}\to\exp z$ by The Limit of a Convergent Complex Sequence (i). Hence, by Limits of Complex Sequences: Uniqueness, Real and Imaginary Parts, Arithmetic, Real Sequences, Conjugates, Moduli, the Cauchy Criterion and the Modulus Metric (i), for $w\in\mathbb{C}$,

$$P_{T_{z}}\to w\quad\text{if and only if}\quad w=\exp z.$$

Let $\mu(F,\mathbb{C},\mathbb{C})$ be the 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), with bound variables distinct from those above, which holds exactly when $F$ is a map $F:\mathbb{C}\to\mathbb{C}$, and let

$$\varphi=\mu(F,\mathbb{C},\mathbb{C})\wedge\forall z\,\forall w\,\forall t\,\forall s\,\bigl(((z,w)\in F\wedge\theta(z,t)\wedge\pi(t,s))\Rightarrow\kappa(s,w)\bigr).$$

Assign to $F$ a map $\mathbb{C}\to\mathbb{C}$. By Maps between Classes: Values, Pairs, Extensionality, Restrictions, Constant Maps and Preimages (ii) and the paragraphs on the terms and on partial sums, the premises of the implication say that $z\in\mathbb{C}$, $w=F(z)$, $t=T_{z}$ and $s=P_{T_{z}}$, which exist for every $z\in\mathbb{C}$ and are sets, $F(z)$ as an element of $\mathbb{C}$ and $T_{z}$ and $P_{T_{z}}$ as sequences in $\mathbb{C}$; and then $\kappa(s,w)$ says $P_{T_{z}}\to F(z)$, as $F(z)\in\mathbb{C}$, that is, $F(z)=\exp z$. So $\varphi$ holds if and only if $F$ is a map $\mathbb{C}\to\mathbb{C}$ with $F(z)=\exp z$ for every $z\in\mathbb{C}$. As $\exp$ is such a map (The Complex Exponential Function (i)), this holds if and only if $F=\exp$, by Maps between Classes: Values, Pairs, Extensionality, Restrictions, Constant Maps and Preimages (iii). Thus $\varphi$, whose only free variable other than parameters is $F$, that is $x_{0}$, is a predicative formula in $x_{0}$ in the sense of Renaming and Substituting Variables in Predicative Formulas, and it holds exactly when $x_{0}$ is the complex exponential function.

Any position. By Renaming and Substituting Variables in Predicative Formulas (i) with $k=1$ and $\sigma(0)=i$, the formula $\varphi(x_{i})$ is a predicative formula in $x_{0},\dots,x_{n-1}$ that holds, under every assignment of sets to $x_{0},\dots,x_{n-1}$, exactly when $x_{i}$ is the complex exponential function. This proves (i).

The class. The Class Comprehension Theorem for Predicative Formulas (i), applied to $\varphi$ with $x_{0}$ as its single variable and the parameters of the statement as its parameters, gives a class $E$ whose set elements are exactly the sets that are the complex exponential function. It serves as the $E$ of (ii), since every element of a class is a set, and so is $\exp$, a map $\mathbb{C}\to\mathbb{C}$.