Theorem absefib

Description: A complex number is real iff the exponential of its product with _i has absolute value one. (Contributed by NM, 21-Aug-2008)

	Ref	Expression
Assertion	absefib	$$⊢A\in ℂ\to \left(A\in ℝ\leftrightarrow \left|{\mathrm{e}}^{\mathrm{i}A}\right|=1\right)$$

Proof

Step	Hyp	Ref	Expression
1		ef0	$$⊢{\mathrm{e}}^0=1$$
2	1	eqeq2i	$$⊢{\mathrm{e}}^{-\Im \left(A\right)}={\mathrm{e}}^0\leftrightarrow {\mathrm{e}}^{-\Im \left(A\right)}=1$$
3		imcl	$$⊢A\in ℂ\to \Im \left(A\right)\in ℝ$$
4	3	renegcld	$$⊢A\in ℂ\to -\Im \left(A\right)\in ℝ$$
5		0re	$$⊢0\in ℝ$$
6		reef11	$$⊢\left(-\Im \left(A\right)\in ℝ\wedge 0\in ℝ\right)\to \left({\mathrm{e}}^{-\Im \left(A\right)}={\mathrm{e}}^0\leftrightarrow -\Im \left(A\right)=0\right)$$
7	4 5 6	sylancl	$$⊢A\in ℂ\to \left({\mathrm{e}}^{-\Im \left(A\right)}={\mathrm{e}}^0\leftrightarrow -\Im \left(A\right)=0\right)$$
8	2 7	bitr3id	$$⊢A\in ℂ\to \left({\mathrm{e}}^{-\Im \left(A\right)}=1\leftrightarrow -\Im \left(A\right)=0\right)$$
9	3	recnd	$$⊢A\in ℂ\to \Im \left(A\right)\in ℂ$$
10	9	negeq0d	$$⊢A\in ℂ\to \left(\Im \left(A\right)=0\leftrightarrow -\Im \left(A\right)=0\right)$$
11	8 10	bitr4d	$$⊢A\in ℂ\to \left({\mathrm{e}}^{-\Im \left(A\right)}=1\leftrightarrow \Im \left(A\right)=0\right)$$
12		ax-icn	$$⊢\mathrm{i}\in ℂ$$
13		mulcl	$$⊢\left(\mathrm{i}\in ℂ\wedge A\in ℂ\right)\to \mathrm{i}A\in ℂ$$
14	12 13	mpan	$$⊢A\in ℂ\to \mathrm{i}A\in ℂ$$
15		absef	$$⊢\mathrm{i}A\in ℂ\to \left|{\mathrm{e}}^{\mathrm{i}A}\right|={\mathrm{e}}^{\Re \left(\mathrm{i}A\right)}$$
16	14 15	syl	$$⊢A\in ℂ\to \left|{\mathrm{e}}^{\mathrm{i}A}\right|={\mathrm{e}}^{\Re \left(\mathrm{i}A\right)}$$
17		recl	$$⊢A\in ℂ\to \Re \left(A\right)\in ℝ$$
18	17	recnd	$$⊢A\in ℂ\to \Re \left(A\right)\in ℂ$$
19		mulcl	$$⊢\left(\mathrm{i}\in ℂ\wedge \Im \left(A\right)\in ℂ\right)\to \mathrm{i}\Im \left(A\right)\in ℂ$$
20	12 9 19	sylancr	$$⊢A\in ℂ\to \mathrm{i}\Im \left(A\right)\in ℂ$$
21		replim	$$⊢A\in ℂ\to A=\Re \left(A\right)+\mathrm{i}\Im \left(A\right)$$
22	18 20 21	comraddd	$$⊢A\in ℂ\to A=\mathrm{i}\Im \left(A\right)+\Re \left(A\right)$$
23	22	oveq2d	$$⊢A\in ℂ\to \mathrm{i}A=\mathrm{i}\left(\mathrm{i}\Im \left(A\right)+\Re \left(A\right)\right)$$
24		adddi	$$⊢\left(\mathrm{i}\in ℂ\wedge \mathrm{i}\Im \left(A\right)\in ℂ\wedge \Re \left(A\right)\in ℂ\right)\to \mathrm{i}\left(\mathrm{i}\Im \left(A\right)+\Re \left(A\right)\right)=\mathrm{i}\mathrm{i}\Im \left(A\right)+\mathrm{i}\Re \left(A\right)$$
25	12 20 18 24	mp3an2i	$$⊢A\in ℂ\to \mathrm{i}\left(\mathrm{i}\Im \left(A\right)+\Re \left(A\right)\right)=\mathrm{i}\mathrm{i}\Im \left(A\right)+\mathrm{i}\Re \left(A\right)$$
26		ixi	$$⊢\mathrm{i}\mathrm{i}=-1$$
27	26	oveq1i	$$⊢\mathrm{i}\mathrm{i}\Im \left(A\right)=-1\Im \left(A\right)$$
28		mulass	$$⊢\left(\mathrm{i}\in ℂ\wedge \mathrm{i}\in ℂ\wedge \Im \left(A\right)\in ℂ\right)\to \mathrm{i}\mathrm{i}\Im \left(A\right)=\mathrm{i}\mathrm{i}\Im \left(A\right)$$
29	12 12 9 28	mp3an12i	$$⊢A\in ℂ\to \mathrm{i}\mathrm{i}\Im \left(A\right)=\mathrm{i}\mathrm{i}\Im \left(A\right)$$
30	9	mulm1d	$$⊢A\in ℂ\to -1\Im \left(A\right)=-\Im \left(A\right)$$
31	27 29 30	3eqtr3a	$$⊢A\in ℂ\to \mathrm{i}\mathrm{i}\Im \left(A\right)=-\Im \left(A\right)$$
32	31	oveq1d	$$⊢A\in ℂ\to \mathrm{i}\mathrm{i}\Im \left(A\right)+\mathrm{i}\Re \left(A\right)=-\Im \left(A\right)+\mathrm{i}\Re \left(A\right)$$
33	25 32	eqtrd	$$⊢A\in ℂ\to \mathrm{i}\left(\mathrm{i}\Im \left(A\right)+\Re \left(A\right)\right)=-\Im \left(A\right)+\mathrm{i}\Re \left(A\right)$$
34	23 33	eqtrd	$$⊢A\in ℂ\to \mathrm{i}A=-\Im \left(A\right)+\mathrm{i}\Re \left(A\right)$$
35	34	fveq2d	$$⊢A\in ℂ\to \Re \left(\mathrm{i}A\right)=\Re \left(-\Im \left(A\right)+\mathrm{i}\Re \left(A\right)\right)$$
36	4 17	crred	$$⊢A\in ℂ\to \Re \left(-\Im \left(A\right)+\mathrm{i}\Re \left(A\right)\right)=-\Im \left(A\right)$$
37	35 36	eqtrd	$$⊢A\in ℂ\to \Re \left(\mathrm{i}A\right)=-\Im \left(A\right)$$
38	37	fveq2d	$$⊢A\in ℂ\to {\mathrm{e}}^{\Re \left(\mathrm{i}A\right)}={\mathrm{e}}^{-\Im \left(A\right)}$$
39	16 38	eqtrd	$$⊢A\in ℂ\to \left|{\mathrm{e}}^{\mathrm{i}A}\right|={\mathrm{e}}^{-\Im \left(A\right)}$$
40	39	eqeq1d	$$⊢A\in ℂ\to \left(\left|{\mathrm{e}}^{\mathrm{i}A}\right|=1\leftrightarrow {\mathrm{e}}^{-\Im \left(A\right)}=1\right)$$
41		reim0b	$$⊢A\in ℂ\to \left(A\in ℝ\leftrightarrow \Im \left(A\right)=0\right)$$
42	11 40 41	3bitr4rd	$$⊢A\in ℂ\to \left(A\in ℝ\leftrightarrow \left|{\mathrm{e}}^{\mathrm{i}A}\right|=1\right)$$