Theorem efeul

Description: Eulerian representation of the complex exponential. (Suggested by Jeff Hankins, 3-Jul-2006.) (Contributed by NM, 4-Jul-2006)

	Ref	Expression
Assertion	efeul	$$⊢A\in ℂ\to {\mathrm{e}}^A={\mathrm{e}}^{\Re \left(A\right)}\left(\cos \Im \left(A\right)+\mathrm{i}\sin \Im \left(A\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		replim	$$⊢A\in ℂ\to A=\Re \left(A\right)+\mathrm{i}\Im \left(A\right)$$
2	1	fveq2d	$$⊢A\in ℂ\to {\mathrm{e}}^A={\mathrm{e}}^{\Re \left(A\right)+\mathrm{i}\Im \left(A\right)}$$
3		recl	$$⊢A\in ℂ\to \Re \left(A\right)\in ℝ$$
4	3	recnd	$$⊢A\in ℂ\to \Re \left(A\right)\in ℂ$$
5		ax-icn	$$⊢\mathrm{i}\in ℂ$$
6		imcl	$$⊢A\in ℂ\to \Im \left(A\right)\in ℝ$$
7	6	recnd	$$⊢A\in ℂ\to \Im \left(A\right)\in ℂ$$
8		mulcl	$$⊢\left(\mathrm{i}\in ℂ\wedge \Im \left(A\right)\in ℂ\right)\to \mathrm{i}\Im \left(A\right)\in ℂ$$
9	5 7 8	sylancr	$$⊢A\in ℂ\to \mathrm{i}\Im \left(A\right)\in ℂ$$
10		efadd	$$⊢\left(\Re \left(A\right)\in ℂ\wedge \mathrm{i}\Im \left(A\right)\in ℂ\right)\to {\mathrm{e}}^{\Re \left(A\right)+\mathrm{i}\Im \left(A\right)}={\mathrm{e}}^{\Re \left(A\right)}{\mathrm{e}}^{\mathrm{i}\Im \left(A\right)}$$
11	4 9 10	syl2anc	$$⊢A\in ℂ\to {\mathrm{e}}^{\Re \left(A\right)+\mathrm{i}\Im \left(A\right)}={\mathrm{e}}^{\Re \left(A\right)}{\mathrm{e}}^{\mathrm{i}\Im \left(A\right)}$$
12		efival	$$⊢\Im \left(A\right)\in ℂ\to {\mathrm{e}}^{\mathrm{i}\Im \left(A\right)}=\cos \Im \left(A\right)+\mathrm{i}\sin \Im \left(A\right)$$
13	7 12	syl	$$⊢A\in ℂ\to {\mathrm{e}}^{\mathrm{i}\Im \left(A\right)}=\cos \Im \left(A\right)+\mathrm{i}\sin \Im \left(A\right)$$
14	13	oveq2d	$$⊢A\in ℂ\to {\mathrm{e}}^{\Re \left(A\right)}{\mathrm{e}}^{\mathrm{i}\Im \left(A\right)}={\mathrm{e}}^{\Re \left(A\right)}\left(\cos \Im \left(A\right)+\mathrm{i}\sin \Im \left(A\right)\right)$$
15	2 11 14	3eqtrd	$$⊢A\in ℂ\to {\mathrm{e}}^A={\mathrm{e}}^{\Re \left(A\right)}\left(\cos \Im \left(A\right)+\mathrm{i}\sin \Im \left(A\right)\right)$$