Proof of The Complex Exponential Is Holomorphic and Is Its Own Derivative

Routine facts of arithmetic and about maps are used without comment (Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity); in particular, two maps on the same domain with the same values are equal (Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (iv)).

Step 1: the plane is open. The whole plane $\mathbb{C}$ is open in $(\mathbb{C},d_{\mathbb{C}})$ by Open Subset of a Metric Space (i): about any $z\in\mathbb{C}$ the ball $B_{d_{\mathbb{C}}}(z,1)$ is a subset of $\mathbb{C}$, as every open ball of this metric space is. Hence The Complex Derivative at a Point (i) and Holomorphic Functions and Their Derivatives (i) apply to $\exp$ with $U=W=\mathbb{C}$.

Step 2: a linear bound on the difference quotient. Fix $z\in\mathbb{C}$ and put

$$K=e\,|\exp z|+1 .$$

This is a positive real number: $e=\exp_{\mathbb{R}}(1)$ (The Real Exponential Function (iii)) is positive because the real exponential takes positive values (Basic Properties of the Exponential Function (iii)), and $|\exp z|\ge0$ (Conjugation and Modulus of Complex Numbers: Field Automorphism, Real and Imaginary Parts, Multiplicativity, Inverses, Component Bounds, Triangle Inequalities and Finite Sums (iii)). Now let $h\in\mathbb{C}$ with $0<|h|<1$. Since the real exponential is increasing (Basic Properties of the Exponential Function (ix)), $\exp_{\mathbb{R}}(|h|)<\exp_{\mathbb{R}}(1)=e$. The estimate for difference quotients (Estimates for the Complex Exponential and Its Continuity (iii)) therefore gives

$$\Bigl|\frac{\exp(z+h)-\exp z}{h}-\exp z\Bigr|\le|\exp z|\,|h|\,\exp_{\mathbb{R}}(|h|)\le e\,|\exp z|\,|h|\le K\,|h| .$$

Step 3: the derivative at $z$. Let $\varepsilon>0$ be given. With $z$ and $K$ fixed as in Step 2, choose

$$\delta=\min(1,\varepsilon/K),$$

a positive real number depending on $\varepsilon$ and on $z$. Let $w\in\mathbb{C}$ with $0<|w-z|<\delta$, and put $h=w-z$, so that $w=z+h$ and $0<|h|<\delta\le1$. By Step 2,

$$\Bigl|\frac{\exp(w)-\exp z}{w-z}-\exp z\Bigr|\le K\,|h|<K\delta\le\varepsilon .$$

So $\exp z$ is a complex derivative of $\exp$ at $z$ (The Complex Derivative at a Point (i)); hence $\exp$ is complex differentiable at $z$, and its complex derivative there is $\exp'(z)=\exp z$ (The Complex Derivative at a Point (ii)).

Step 4: holomorphy and the derivative map. As $z\in\mathbb{C}$ was arbitrary, $\exp$ is complex differentiable at every point of $\mathbb{C}$, that is, holomorphic on $\mathbb{C}$ (Holomorphic Functions and Their Derivatives (i)). Its derivative $\exp':\mathbb{C}\to\mathbb{C}$ (Holomorphic Functions and Their Derivatives (ii)) takes the value $\exp'(z)=\exp z$ at every $z\in\mathbb{C}$ by Step 3, so the two maps $\exp'$ and $\exp$ have the same values and are equal.