Defining the complex exponential I was pondering a bit about how to define the exponential and trigonometric functions. The definitions I find the most appealing seem to be their definitions as the unique solutions to the ODEs : $y'=y,\ y_0=1$; $y''=-y,\ y_0=0/1$ and $y'_0=1/0$.
However, I was wondering if this could be extended as follows:
$e^z:\mathbb{C}\to \mathbb{C}$ is the unique solution to the ODE $\frac{\mathbb{d}}{\mathbb{dz}}f = f$ with $f(0)=1$. Then you define $\cos{x}=\Re(e^{ix})$ and $\sin{x}=\Im(e^{ix})$.
Is there a theorem that allows one to prove the existence of uniqueness in this case?
 A: Setup
It would be simplest to just write down the Taylor Polynomials and show they converge to a solution, but I assume you want to know how one could approach existence and uniqueness without trying to solve for series coefficients (or already having $e^z$ in hand). So, instead, we can follow similar steps to a proof of the Picard–Lindelöf theorem.
This answer is heavily inspired by (paraphrasing?) the discussion in "2.3 The Method of Successive Approximations" from Ordinary Differential Equations in the Complex Domain by Einar Hille, but there is significant simplification in specializing to this case. In other words, I'm not proving the general theorem here, just going through the steps for this ODE.
Existence
The initial value problem is equivalent to $f(z)=1+\int_0^zf(s)\,\mathrm ds$. Define the sequence of approximations $f_0(z)=1$, $f_n(z)=1+\int_0^zf_{n-1}(s)\,\mathrm ds$. These approximations are all entire (and hence there is no issue with the integrals) because they're all polynomials.
Note that $|f_1(z)-f_0|=|1+z-1|=|z|$. Then $|f_2(z)-f_1(z)|=\left|\int_0^zf_{1}(s)-f_{0}(s)\,\mathrm ds\right|\le\left|\int_0^z|s|\,|\mathrm ds|\right|=\frac12|z|^2$. By an induction argument, we have $|f_k(z)-f_{k-1}(z)|\le|z|^k/k!$ . This means that the series $f(z):=1+\displaystyle{\sum_{n=1}^\infty}\left(f_n(z)-f_{n-1}(z)\right)$ converges absolutely and uniformly on any disk. Since $\lim f_n(z)=f(z)$, this is a solution.
Uniqueness
Suppose that $g$ is any solution, and define the sequence of $f_n$ as above. Then \begin{align*}|g(z)-f_n(z)|&=\left|\int_0^z g(s)-f_{n-1}(s)\,\mathrm ds\right|\\&\le\left|\int_0^z |g(s)-f_{n-1}(s)|\,|\mathrm ds|\right|\\&\le\left|\int_0^z |\mathrm ds|\left|\int_0^s|g(t)-f_{n-2}(t)|\,|\mathrm dt|\right|\right|\\&=\left|\int_0^z |s||g(s)-f_{n-2}(s)||\mathrm ds|\right|\\\cdots&\le\dfrac{1}{(n-1)!}\left|\int_0^z |s|^{n-1}|g(s)-1||\mathrm ds|\right|\end{align*}
On any closed disk, $|g(s)-1|$ will be bounded (by $b$, say), so that $|g(z)-f_n(z)|\le b/n!\to0$. Hence $g(z)=f(z)$.
