Theorem absefi

Description: The absolute value of the exponential of an imaginary number is one. Equation 48 of Rudin p. 167. (Contributed by Jason Orendorff, 9-Feb-2007)

	Ref	Expression
Assertion	absefi	$$⊢A\in ℝ\to \left|{\mathrm{e}}^{\mathrm{i}A}\right|=1$$

Proof

Step	Hyp	Ref	Expression
1		recn	$$⊢A\in ℝ\to A\in ℂ$$
2		efival	$$⊢A\in ℂ\to {\mathrm{e}}^{\mathrm{i}A}=\cos A+\mathrm{i}\sin A$$
3	1 2	syl	$$⊢A\in ℝ\to {\mathrm{e}}^{\mathrm{i}A}=\cos A+\mathrm{i}\sin A$$
4	3	fveq2d	$$⊢A\in ℝ\to \left|{\mathrm{e}}^{\mathrm{i}A}\right|=\left|\cos A+\mathrm{i}\sin A\right|$$
5		recoscl	$$⊢A\in ℝ\to \cos A\in ℝ$$
6		resincl	$$⊢A\in ℝ\to \sin A\in ℝ$$
7		absreim	$$⊢\left(\cos A\in ℝ\wedge \sin A\in ℝ\right)\to \left|\cos A+\mathrm{i}\sin A\right|=\sqrt{{\cos A}^2+{\sin A}^2}$$
8	5 6 7	syl2anc	$$⊢A\in ℝ\to \left|\cos A+\mathrm{i}\sin A\right|=\sqrt{{\cos A}^2+{\sin A}^2}$$
9	5	resqcld	$$⊢A\in ℝ\to {\cos A}^2\in ℝ$$
10	9	recnd	$$⊢A\in ℝ\to {\cos A}^2\in ℂ$$
11	6	resqcld	$$⊢A\in ℝ\to {\sin A}^2\in ℝ$$
12	11	recnd	$$⊢A\in ℝ\to {\sin A}^2\in ℂ$$
13	10 12	addcomd	$$⊢A\in ℝ\to {\cos A}^2+{\sin A}^2={\sin A}^2+{\cos A}^2$$
14		sincossq	$$⊢A\in ℂ\to {\sin A}^2+{\cos A}^2=1$$
15	1 14	syl	$$⊢A\in ℝ\to {\sin A}^2+{\cos A}^2=1$$
16	13 15	eqtrd	$$⊢A\in ℝ\to {\cos A}^2+{\sin A}^2=1$$
17	16	fveq2d	$$⊢A\in ℝ\to \sqrt{{\cos A}^2+{\sin A}^2}=\sqrt{1}$$
18		sqrt1	$$⊢\sqrt{1}=1$$
19	17 18	eqtrdi	$$⊢A\in ℝ\to \sqrt{{\cos A}^2+{\sin A}^2}=1$$
20	8 19	eqtrd	$$⊢A\in ℝ\to \left|\cos A+\mathrm{i}\sin A\right|=1$$
21	4 20	eqtrd	$$⊢A\in ℝ\to \left|{\mathrm{e}}^{\mathrm{i}A}\right|=1$$