Proof of Euler's Formula: the Complex Exponential on the Imaginary Axis, Its Modulus and Its Conjugate

Routine facts are used without comment (Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity); results on real and imaginary parts, conjugates and moduli are read for the current complex numbers 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).

Euler's formula. Every complex number is its real part plus $i$ times its imaginary part: $z=\operatorname{Re}z+(\operatorname{Im}z)\,i$ for every $z\in\mathbb{C}$, by Real and Imaginary Parts of a Complex Number (i). We apply this to $z=\exp(it)$. By the definitions of the cosine and the sine (The Real Sine and Cosine Functions (i), The Real Sine and Cosine Functions (ii)), the real part of $\exp(it)$ is $\cos t$ and its imaginary part is $\sin t$. Hence

$$\exp(it)=\cos t+i\sin t ,$$

which is (i).

Unit modulus. By the last assertion of The Complex Exponential: the Functional Equation, Conjugates, Real Arguments and the Modulus (vi), applied with $y=t$, $|\exp(it)|=1$. This is (ii).

The exponential in real coordinates. We split $x+iy$ into the real number $x$ and the purely imaginary number $iy$. The functional equation The Complex Exponential: the Functional Equation, Conjugates, Real Arguments and the Modulus (ii), with $z=x$ and $w=iy$, gives $\exp(x+iy)=\exp x\cdot\exp(iy)$. On the real axis the complex exponential agrees with the real one, $\exp x=\exp_{\mathbb{R}}(x)$, by The Complex Exponential: the Functional Equation, Conjugates, Real Arguments and the Modulus (v); and Euler's formula (i), just proved, applied with $t=y$, gives $\exp(iy)=\cos y+i\sin y$. Together,

$$\exp(x+iy)=\exp x\cdot\exp(iy)=\exp_{\mathbb{R}}(x)\,(\cos y+i\sin y),$$

which is (iii).

Conjugates. We first compute the conjugate of $it$. Since $it=0+t\,i$ with $0$ and $t$ real, the real and imaginary parts of $it$ are $\operatorname{Re}(it)=0$ and $\operatorname{Im}(it)=t$, by the uniqueness in Real and Imaginary Parts of a Complex Number (i). The definition of the conjugate (The Complex Conjugate of a Complex Number (i)) therefore gives $\overline{it}=0-t\,i=-it$. Conjugation commutes with the exponential, by The Complex Exponential: the Functional Equation, Conjugates, Real Arguments and the Modulus (iv) applied with $z=it$, and so

$$\overline{\exp(it)}=\exp\bigl(\overline{it}\bigr)=\exp(-it).$$

This is (iv).