Theorem: Euler's Formula/Real Domain

Let $\theta \in \R$ be a real number.
Then:
:$e^{i \theta} = \cos \theta + i \sin \theta$

Proof:
It follows from Argument of Product equals Sum of Arguments that the $\map \arg z$ function for all $z \in \C$ satisfies the relationship:
:$\map \arg {z_1 z_2} = \map \arg {z_1} + \map \arg {z_2}$
which means that $\map \arg z$ is a kind of logarithm, in the sense that it satisfies the fundamental property of logarithms:
:$\log x y = \log x + \log y$
Notice that $\map \arg z$ can not be considered a generalization to complex values of the ordinary $\log$ function for real values, since for $x \in \R$, we have:
:$0 = \map \arg x \ne \log x$
If we do wish to generalize the $\log$ function to complex values, we can use $\arg z$ to define a set of functions:
:$\map {\operatorname{alog} } z = a \map \arg z + \log \cmod z$
for any $a \in \C$, where $\cmod z$ is the modulus of $z$.
All functions satisfy the fundamental property of logarithms and also coincide with the $\log$ function for all real values.
This is established in the following lemma.
=== Lemma 1 ===
For all $a,z \in \C$, define the (complex valued) function $\operatorname{alog}$ as:
:$\map {\operatorname{alog} } z = a \map \arg z + \log \cmod z$
then, for any $z_1, z_2 \in \C$ and $x \in \R$:
:$\map {\operatorname{alog} } {z_1 z_2} = \map {\operatorname{alog} } {z_1} + \map {\operatorname{alog} } {z_2}$
and:
:$\map {\operatorname{alog} } x = \log x$
This means that our (complex valued) $\operatorname{alog}$ functions can genuinely be considered generalizations of the (real valued) $\log$ function.
=== Proof of Lemma 1 ===
Let $z_1, z_2$ be any two complex numbers, straightforward substitution on the definition of $\operatorname{alog}$ yields:
{{begin-eqn}}
{{eqn | l = \map {\operatorname{alog} } {z_1 z_2}
      | r = a \map \arg {z_1 z_2} + \log \cmod {z_1 z_2}
}}
{{eqn | r = a \paren {\map \arg {z_1} + \map \arg {z_1} } + \map \log {\cmod {z_1} \cmod {z_2} }
}}
{{eqn | r = a \paren {\map \arg {z_1} + \map \arg {z_1} } + \log \cmod {z_1} + \log \cmod {z_2}
}}
{{eqn | r = a \map \arg {z_1} + \log \cmod {z_1} + a \map \arg {z_2} + \log \cmod {z_2}
}}
{{eqn | r = \map {\operatorname{alog} } {z_1} + \map {\operatorname{alog} } {z_1}
}}
{{end-eqn}}
Second part of our lemma is even more straightforward since for $x \in \R$, we have:
:$\map \arg x = 0$
Then:
{{begin-eqn}}
{{eqn | l = \map {\operatorname{alog} } x
      | r = a \map \arg x + \log \cmod x
}}
{{eqn | r = \log x
}}
{{end-eqn}}
which concludes the proof of Lemma 1.
{{qed|lemma}}
We're left  with an infinitude of possible generalizations of the $\log$ function, namely one for each choice of $a$ in our definition of $\operatorname{alog}$.
The following lemma proves that there's a value for $a$ that guarantees our definition of $\operatorname{alog}$ satisfies the much desirable property of $\log$:
:$\dfrac{\d \log x} {\d x} = \dfrac 1 x$
=== Lemma 2 ===
Let $\map {\operatorname{alog} } z = a \map \arg z + \log \cmod z$.
Then if:
:$\dfrac {\map \d {\operatorname{alog} z} } {\d z} = \dfrac 1 z$
we must have:
:$a = i$
=== Proof of Lemma 2 ===
Let $z \in \C$ be such that:
:$\cmod z = 1$
and:
:$\map \arg z = \theta$
Then:
:$z = \cos \theta + i \sin \theta$
Plugging those values in our definition of $\operatorname{alog}$:
{{begin-eqn}}
{{eqn | l = \map {\operatorname{alog} } z
      | r = a \map \arg {\cos \theta + i \sin \theta} + \log \cmod z
}}
{{eqn | r = a \theta + \log 1 = a \theta
}}  
{{end-eqn}}
We now have:
:$a \theta = \map {\operatorname{alog} } {\cos \theta + i \sin \theta}$
Taking the derivative with respect to $\theta$ on both sides, we have:
{{begin-eqn}}
{{eqn | l = \map {\frac \d {\d \theta} } {a \theta}
      | r = \map {\frac \d {\d \theta} } {\map {\operatorname{alog} } {\cos \theta + i \sin \theta} }
}}
{{eqn | l = a
      | r = \dfrac {\map \d {\cos \theta + i \sin \theta} } {\d \theta} \dfrac {\map \d {\map {\operatorname{alog} } {\cos \theta + i \sin \theta} } } {\map \d {\cos \theta + i \sin \theta} }
      | c = Chain Rule for Derivatives
}}
{{eqn | l = a
      | r = \paren {-\sin \theta + i \cos \theta} \frac 1 {\cos \theta + i \sin \theta}
      | c = {{hypothesis}}: $\dfrac {\map \d {\operatorname{alog} z} } {\d z} = \dfrac 1 z$
}}
{{end-eqn}}
This last equation is true regardless of the value of $\theta$.
In particular, for $\theta = 0$, we must have:
:$a = i$
which proves the lemma.
{{qed|lemma}}
We now have established there is one function which truly deserves to be called the logarithm of complex numbers, defined as:
:$\log z = i \map \arg z + \log \cmod z$
Since for any $z, z_1, z_2 \in \C, x \in \R$ it satisfies:
:$\map \log {z_1 z_2} = \log z_1 + \log z_2$
:$\log x = \log x$
:$\dfrac {\map \d {\log z} } {\d z} = \dfrac 1 z$
Let its inverse function be referred to as the '''exponential''' of complex numbers, denoted as $e^z$.
If we write $z$ in its polar form:
:$z = \cmod z \paren {\cos \theta + i \sin \theta}$
we have that:
:$e^{i \theta + \log \cmod z} = \cmod z \paren {\cos \theta + i \sin \theta}$
Consider this equation for any number $z$ such that $\cmod z = 1$.
Then:
:$e^{i \theta} = \cos \theta + i \sin \theta$
{{qed}}