Sketch: the moduli of the terms are the terms of the real exponential series at |z|, so the comparison test gives absolute convergence; the sums then define a function.
Routine facts about numbers, maps and finite sums are used without comment (Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity); the results on conjugates and moduli cited below are read for the present complex numbers, conjugate and modulus 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), 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 (iii) and 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 (iv), and the result on real series in the present definitions of sequences and series by The Earlier and the New Versions of the Definitions of Sequences, Limits, Cauchy Sequences, Series and Iterated Operations Agree (i) and The Earlier and the New Versions of the Definitions of Sequences, Limits, Cauchy Sequences, Series and Iterated Operations Agree (v).
Fix and write
The terms. Writing exhibits as the -th term of the power series at whose coefficients form a sequence in (Complex Power Series: the Sequence of Terms and the Sum as a Function on the Set of Convergence (ii)). Hence the numbers are the terms of exactly one sequence in (Complex Power Series: the Sequence of Terms and the Sum as a Function on the Set of Convergence (i)). As was arbitrary, this proves (i).
Absolute convergence. We compute the moduli of the terms. The modulus is multiplicative (Conjugation and Modulus of Complex Numbers: Field Automorphism, Real and Imaginary Parts, Multiplicativity, Inverses, Component Bounds, Triangle Inequalities and Finite Sums (iv)), the modulus of a power is the power of the modulus, for , by induction on from (The Modulus of a Complex Number (ii)) and (Powers in a Commutative Ring, a Field and an Ordered Field: Exponent Laws, Factorisation, Geometric Sums, Monotonicity and Bernoulli's Inequality (i), Powers in a Commutative Ring, a Field and an Ordered Field: Exponent Laws, Factorisation, Geometric Sums, Monotonicity and Bernoulli's Inequality (ii), Conjugation and Modulus of Complex Numbers: Field Automorphism, Real and Imaginary Parts, Multiplicativity, Inverses, Component Bounds, Triangle Inequalities and Finite Sums (iv)), and the modulus of a reciprocal is the reciprocal of the modulus (Conjugation and Modulus of Complex Numbers: Field Automorphism, Real and Imaginary Parts, Multiplicativity, Inverses, Component Bounds, Triangle Inequalities and Finite Sums (v)). Finally is a nonnegative real number, and the modulus of a real number is its absolute value (The Modulus of a Complex Number (ii)), so . Together,
The right-hand side is the -th term of the real exponential series at , and that series converges (The Exponential Series Converges Absolutely, and Its Sum Is a Map on β (ii)). Thus the series of moduli converges, which is to say that converges absolutely (Series of Complex Numbers: Partial Sums, Convergence, the Sum and Absolute Convergence (iii)); and an absolutely convergent series in converges (Series of Complex Numbers: Absolute Convergence, Comparison, Linearity, Index Shifts, Real and Imaginary Parts, Conjugates, Real Series and the Cauchy Product (i)). As was arbitrary, this proves (ii).
The sum as a function. By the previous paragraph the series of (i) converges at every point of . Applying Complex Power Series: the Sequence of Terms and the Sum as a Function on the Set of Convergence (iii) with and the coefficients , the sums of these series are the values of exactly one function , namely
This proves (iii).
Loadingβ¦