Proof of Complex Power Series: the Sequence of Terms and the Sum as a Function on the Set of Convergence

Throughout, the result on limits in metric spaces cited below is read in the current definitions of sequences, metric spaces, convergence and limits (The Earlier and the New Versions of the Definitions of Sequences, Limits, Cauchy Sequences, Series and Iterated Operations Agree (i), The Earlier and the New Versions of the Definitions of Metric Spaces, Convergence, Continuity and Compactness Agree (i), The Earlier and the New Versions of the Definitions of Metric Spaces, Convergence, Continuity and Compactness Agree (iii), The Earlier and the New Versions of the Definitions of Metric Spaces, Convergence, Continuity and Compactness Agree (iv)).

Uniqueness. $\mathbb{C}$ is a field (The Complex Numbers: Pairs of Real Numbers with Their Addition and Multiplication, and the Imaginary Unit (v)), hence a commutative ring (Fields (i)). A sequence in $\mathbb{C}$ is a map $\mathbb{N}\to\mathbb{C}$ (Sequences (i)), and two maps with the same values are equal. So the sequences of (i) and (ii) are unique once they exist, and only their existence is shown below.

The predecessor map. For $k\in\mathbb{N}$ we have $1\le k$ (Arithmetic and Order of the Natural Numbers (x)), so $k-1$ is the only $j\in\mathbb{N}_{0}$ with $((1,j),k)\in{+}$ for the addition of $\mathbb{N}_{0}$ (The Difference of Two Natural Numbers with Zero (i)). This condition on $k$ and $j$ is predicative (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)), so by Maps from Functional Predicative Relations, and Families of Sections (ii) there is a map $\pi:\mathbb{N}\to\mathbb{N}_{0}$ with $\pi(k)=k-1$ for every $k\in\mathbb{N}$.

Proof of (i). Let $u\in\mathbb{C}$. By Maps Given by Iterated Operations: Partial Iterates, Images of Natural Numbers, Powers and Operations over a Finite Set (iv) there is a map $P:\mathbb{N}_{0}\to\mathbb{C}$ with $P(n)=u^{n}$, so $P\circ\pi$ is a sequence in $\mathbb{C}$ with $k$-th term $u^{k-1}$ (Basic Properties of Functions: Equality, Composition, Identity, Inverse and Restriction (ii)). Combining $(c_{k})$ and $P\circ\pi$ through the multiplication $\mathbb{C}\times\mathbb{C}\to\mathbb{C}$ gives a sequence in $\mathbb{C}$ with $k$-th term $c_{k}u^{k-1}$ (Composite Maps into Classes, Images of Singletons, and Agreement of Maps by Induction (i)).

Proof of (ii). Let $n\in\mathbb{N}_{0}$. Read in $\mathbb{C}$, $n!$ is $\iota$ of $n!$ read in $\mathbb{R}$ (The Complex Numbers, with the Real Numbers Identified with a Subset of the Complex Numbers (iv)). The latter is nonzero (Natural Numbers and Factorials Read in the Reals: the Order Carries Over, One Is Least, and Factorials Are Positive, Recursive and Nondecreasing (iii)), and $\iota$ is injective with $\iota(0)=0$ (The Complex Numbers, with the Real Numbers Identified with a Subset of the Complex Numbers (iv)); so $n!\neq0$ in $\mathbb{C}$.

For the sequence, The Factorial as a Map on the Natural Numbers with Zero (i) gives a map $F:\mathbb{N}_{0}\to\mathbb{N}_{0}$ with $F(n)=n!$, and Maps Given by Iterated Operations: Partial Iterates, Images of Natural Numbers, Powers and Operations over a Finite Set (ii), with $R=\mathbb{C}$, a map $\nu:\mathbb{N}_{0}\to\mathbb{C}$ sending each $n$ to its image in $\mathbb{C}$; so $\chi=\nu\circ F:\mathbb{N}_{0}\to\mathbb{C}$ has $\chi(n)=n!$ read in $\mathbb{C}$. The condition $y\cdot\chi(n)=1$ on $n$ and $y$ is predicative (Typed Terms under a Predicative Guard: Variables, Parameters, Values of Maps and Ordered Pairs, and Predicative Equations and Memberships between Them (iii), Typed Terms under a Predicative Guard: Variables, Parameters, Values of Maps and Ordered Pairs, and Predicative Equations and Memberships between Them (v)), and since $\chi(n)\neq0$ and $\mathbb{C}$ is a field, exactly one $y\in\mathbb{C}$ satisfies it for each $n\in\mathbb{N}_{0}$, namely $1/n!$. By Maps from Functional Predicative Relations, and Families of Sections (ii) there is a map $\rho:\mathbb{N}_{0}\to\mathbb{C}$ with $\rho(n)=1/n!$, and $\rho\circ\pi$ is a sequence in $\mathbb{C}$ with $k$-th term $1/(k-1)!$.

Proof of (iii): a formula for the sums up to $n$. For $u\in\mathbb{C}$ let $(a_{k}(u))$ be the sequence of (i), and $\sigma(u)$ its sequence of partial sums, which exists by Maps Given by Iterated Operations: Partial Iterates, Images of Natural Numbers, Powers and Operations over a Finite Set (i) with the addition of $\mathbb{C}$. By Iterated Operations over Finite Sets: Singletons, Disjoint Unions, Reindexing, Products of Sets, Termwise Combination, Homomorphisms and Intervals (vii), $s=\sigma(u)$ satisfies

$$s:\mathbb{N}\to\mathbb{C},\qquad s(1)=c_{1},\qquad s(n+1)=s(n)+c_{n+1}u^{n}\quad\text{for every }n\in\mathbb{N},$$

the equation $s(1)=c_{1}$ because $u^{0}=1$ (Maps Given by Iterated Operations: Partial Iterates, Images of Natural Numbers, Powers and Operations over a Finite Set (iv)); and by induction on $n$ (Induction for Predicative Formulas, and the Order of ℕ below 1 and below n+1 (i)) it is the only set that does. This condition on $u$ and $s$ is predicative: the map condition 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 (vii); the equations between values of maps, sums and products by Typed Terms under a Predicative Guard: Variables, Parameters, Values of Maps and Ordered Pairs, and Predicative Equations and Memberships between Them (v); the successor $n+1$ of $n$ (Order and Arithmetic of ℕ₀ in Flat Form (ii)) by Atomic Predicative Formulas: Equality with Unordered Pairs, Singletons and Successors (iii) and the power $u^{n}$ by Powers with a Variable Base: a Predicative Formula and the Map (x, m) ↦ x^m (i), both eliminated as in Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (ii). So $\sigma(u)$ is an expression in $u$ in the sense of Maps and Relations Given by Formulas (i).

Proof of (iii): the sum map. Let $u\in D$. By hypothesis $\sigma(u)$ is convergent, with limit $\sum_{k=1}^{\infty}c_{k}u^{k-1}$ (Series of Complex Numbers: Partial Sums, Convergence, the Sum and Absolute Convergence (ii)); by Limits of Complex Sequences: Uniqueness, Real and Imaginary Parts, Arithmetic, Real Sequences, Conjugates, Moduli, the Cauchy Criterion and the Modulus Metric (vii) it converges to this sum also in the metric space $(\mathbb{C},d_{\mathbb{C}})$ of Metric Spaces: Balls, the Metric Topology, and the Real and Complex Numbers as Metric Spaces (v). $D$ is a set, being a subclass of the set $\mathbb{C}$ (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)). So Predicative Formulas for Convergence and Limits, and Maps Defined by Limits (v), with $(\mathbb{C},d_{\mathbb{C}})$ for $(X,d)$, $D$ for $a$ and $\sigma(u)$ for $t(u)$, gives exactly one function $h:D\to\mathbb{C}$ with

$$h(u)=\lim\sigma(u)=\sum_{k=1}^{\infty}c_{k}u^{k-1}\qquad(u\in D).$$