Theorem absef

Description: The absolute value of the exponential is the exponential of the real part. (Contributed by Paul Chapman, 13-Sep-2007)

	Ref	Expression
Assertion	absef	$$⊢A\in ℂ\to \left|{\mathrm{e}}^A\right|={\mathrm{e}}^{\Re \left(A\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	2 11	eqtrd	$$⊢A\in ℂ\to {\mathrm{e}}^A={\mathrm{e}}^{\Re \left(A\right)}{\mathrm{e}}^{\mathrm{i}\Im \left(A\right)}$$
13	12	fveq2d	$$⊢A\in ℂ\to \left|{\mathrm{e}}^A\right|=\left|{\mathrm{e}}^{\Re \left(A\right)}{\mathrm{e}}^{\mathrm{i}\Im \left(A\right)}\right|$$
14	3	reefcld	$$⊢A\in ℂ\to {\mathrm{e}}^{\Re \left(A\right)}\in ℝ$$
15	14	recnd	$$⊢A\in ℂ\to {\mathrm{e}}^{\Re \left(A\right)}\in ℂ$$
16		efcl	$$⊢\mathrm{i}\Im \left(A\right)\in ℂ\to {\mathrm{e}}^{\mathrm{i}\Im \left(A\right)}\in ℂ$$
17	9 16	syl	$$⊢A\in ℂ\to {\mathrm{e}}^{\mathrm{i}\Im \left(A\right)}\in ℂ$$
18	15 17	absmuld	$$⊢A\in ℂ\to \left|{\mathrm{e}}^{\Re \left(A\right)}{\mathrm{e}}^{\mathrm{i}\Im \left(A\right)}\right|=\left|{\mathrm{e}}^{\Re \left(A\right)}\right|\left|{\mathrm{e}}^{\mathrm{i}\Im \left(A\right)}\right|$$
19		absefi	$$⊢\Im \left(A\right)\in ℝ\to \left|{\mathrm{e}}^{\mathrm{i}\Im \left(A\right)}\right|=1$$
20	6 19	syl	$$⊢A\in ℂ\to \left|{\mathrm{e}}^{\mathrm{i}\Im \left(A\right)}\right|=1$$
21	20	oveq2d	$$⊢A\in ℂ\to \left|{\mathrm{e}}^{\Re \left(A\right)}\right|\left|{\mathrm{e}}^{\mathrm{i}\Im \left(A\right)}\right|=\left|{\mathrm{e}}^{\Re \left(A\right)}\right|\cdot 1$$
22	13 18 21	3eqtrd	$$⊢A\in ℂ\to \left|{\mathrm{e}}^A\right|=\left|{\mathrm{e}}^{\Re \left(A\right)}\right|\cdot 1$$
23	15	abscld	$$⊢A\in ℂ\to \left|{\mathrm{e}}^{\Re \left(A\right)}\right|\in ℝ$$
24	23	recnd	$$⊢A\in ℂ\to \left|{\mathrm{e}}^{\Re \left(A\right)}\right|\in ℂ$$
25	24	mulid1d	$$⊢A\in ℂ\to \left|{\mathrm{e}}^{\Re \left(A\right)}\right|\cdot 1=\left|{\mathrm{e}}^{\Re \left(A\right)}\right|$$
26		efgt0	$$⊢\Re \left(A\right)\in ℝ\to 0<{\mathrm{e}}^{\Re \left(A\right)}$$
27	3 26	syl	$$⊢A\in ℂ\to 0<{\mathrm{e}}^{\Re \left(A\right)}$$
28		0re	$$⊢0\in ℝ$$
29		ltle	$$⊢\left(0\in ℝ\wedge {\mathrm{e}}^{\Re \left(A\right)}\in ℝ\right)\to \left(0<{\mathrm{e}}^{\Re \left(A\right)}\to 0\le {\mathrm{e}}^{\Re \left(A\right)}\right)$$
30	28 14 29	sylancr	$$⊢A\in ℂ\to \left(0<{\mathrm{e}}^{\Re \left(A\right)}\to 0\le {\mathrm{e}}^{\Re \left(A\right)}\right)$$
31	27 30	mpd	$$⊢A\in ℂ\to 0\le {\mathrm{e}}^{\Re \left(A\right)}$$
32	14 31	absidd	$$⊢A\in ℂ\to \left|{\mathrm{e}}^{\Re \left(A\right)}\right|={\mathrm{e}}^{\Re \left(A\right)}$$
33	22 25 32	3eqtrd	$$⊢A\in ℂ\to \left|{\mathrm{e}}^A\right|={\mathrm{e}}^{\Re \left(A\right)}$$