Theorem efieq1re

Description: A number whose imaginary exponential is one is real. (Contributed by NM, 21-Aug-2008)

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

Proof

Step	Hyp	Ref	Expression
1		replim	$$⊢A\in ℂ\to A=\Re \left(A\right)+\mathrm{i}\Im \left(A\right)$$
2	1	oveq2d	$$⊢A\in ℂ\to \mathrm{i}A=\mathrm{i}\left(\Re \left(A\right)+\mathrm{i}\Im \left(A\right)\right)$$
3		ax-icn	$$⊢\mathrm{i}\in ℂ$$
4		recl	$$⊢A\in ℂ\to \Re \left(A\right)\in ℝ$$
5	4	recnd	$$⊢A\in ℂ\to \Re \left(A\right)\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	3 7 8	sylancr	$$⊢A\in ℂ\to \mathrm{i}\Im \left(A\right)\in ℂ$$
10		adddi	$$⊢\left(\mathrm{i}\in ℂ\wedge \Re \left(A\right)\in ℂ\wedge \mathrm{i}\Im \left(A\right)\in ℂ\right)\to \mathrm{i}\left(\Re \left(A\right)+\mathrm{i}\Im \left(A\right)\right)=\mathrm{i}\Re \left(A\right)+\mathrm{i}\mathrm{i}\Im \left(A\right)$$
11	3 5 9 10	mp3an2i	$$⊢A\in ℂ\to \mathrm{i}\left(\Re \left(A\right)+\mathrm{i}\Im \left(A\right)\right)=\mathrm{i}\Re \left(A\right)+\mathrm{i}\mathrm{i}\Im \left(A\right)$$
12		ixi	$$⊢\mathrm{i}\mathrm{i}=-1$$
13	12	oveq1i	$$⊢\mathrm{i}\mathrm{i}\Im \left(A\right)=-1\Im \left(A\right)$$
14		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)$$
15	3 3 7 14	mp3an12i	$$⊢A\in ℂ\to \mathrm{i}\mathrm{i}\Im \left(A\right)=\mathrm{i}\mathrm{i}\Im \left(A\right)$$
16	7	mulm1d	$$⊢A\in ℂ\to -1\Im \left(A\right)=-\Im \left(A\right)$$
17	13 15 16	3eqtr3a	$$⊢A\in ℂ\to \mathrm{i}\mathrm{i}\Im \left(A\right)=-\Im \left(A\right)$$
18	17	oveq2d	$$⊢A\in ℂ\to \mathrm{i}\Re \left(A\right)+\mathrm{i}\mathrm{i}\Im \left(A\right)=\mathrm{i}\Re \left(A\right)+\left(-\Im \left(A\right)\right)$$
19	11 18	eqtrd	$$⊢A\in ℂ\to \mathrm{i}\left(\Re \left(A\right)+\mathrm{i}\Im \left(A\right)\right)=\mathrm{i}\Re \left(A\right)+\left(-\Im \left(A\right)\right)$$
20	2 19	eqtrd	$$⊢A\in ℂ\to \mathrm{i}A=\mathrm{i}\Re \left(A\right)+\left(-\Im \left(A\right)\right)$$
21	20	fveq2d	$$⊢A\in ℂ\to {\mathrm{e}}^{\mathrm{i}A}={\mathrm{e}}^{\mathrm{i}\Re \left(A\right)+\left(-\Im \left(A\right)\right)}$$
22		mulcl	$$⊢\left(\mathrm{i}\in ℂ\wedge \Re \left(A\right)\in ℂ\right)\to \mathrm{i}\Re \left(A\right)\in ℂ$$
23	3 5 22	sylancr	$$⊢A\in ℂ\to \mathrm{i}\Re \left(A\right)\in ℂ$$
24	6	renegcld	$$⊢A\in ℂ\to -\Im \left(A\right)\in ℝ$$
25	24	recnd	$$⊢A\in ℂ\to -\Im \left(A\right)\in ℂ$$
26		efadd	$$⊢\left(\mathrm{i}\Re \left(A\right)\in ℂ\wedge -\Im \left(A\right)\in ℂ\right)\to {\mathrm{e}}^{\mathrm{i}\Re \left(A\right)+\left(-\Im \left(A\right)\right)}={\mathrm{e}}^{\mathrm{i}\Re \left(A\right)}{\mathrm{e}}^{-\Im \left(A\right)}$$
27	23 25 26	syl2anc	$$⊢A\in ℂ\to {\mathrm{e}}^{\mathrm{i}\Re \left(A\right)+\left(-\Im \left(A\right)\right)}={\mathrm{e}}^{\mathrm{i}\Re \left(A\right)}{\mathrm{e}}^{-\Im \left(A\right)}$$
28	21 27	eqtrd	$$⊢A\in ℂ\to {\mathrm{e}}^{\mathrm{i}A}={\mathrm{e}}^{\mathrm{i}\Re \left(A\right)}{\mathrm{e}}^{-\Im \left(A\right)}$$
29	28	eqeq1d	$$⊢A\in ℂ\to \left({\mathrm{e}}^{\mathrm{i}A}=1\leftrightarrow {\mathrm{e}}^{\mathrm{i}\Re \left(A\right)}{\mathrm{e}}^{-\Im \left(A\right)}=1\right)$$
30		efcl	$$⊢\mathrm{i}\Re \left(A\right)\in ℂ\to {\mathrm{e}}^{\mathrm{i}\Re \left(A\right)}\in ℂ$$
31	23 30	syl	$$⊢A\in ℂ\to {\mathrm{e}}^{\mathrm{i}\Re \left(A\right)}\in ℂ$$
32		efcl	$$⊢-\Im \left(A\right)\in ℂ\to {\mathrm{e}}^{-\Im \left(A\right)}\in ℂ$$
33	25 32	syl	$$⊢A\in ℂ\to {\mathrm{e}}^{-\Im \left(A\right)}\in ℂ$$
34	31 33	absmuld	$$⊢A\in ℂ\to \left|{\mathrm{e}}^{\mathrm{i}\Re \left(A\right)}{\mathrm{e}}^{-\Im \left(A\right)}\right|=\left|{\mathrm{e}}^{\mathrm{i}\Re \left(A\right)}\right|\left|{\mathrm{e}}^{-\Im \left(A\right)}\right|$$
35		absefi	$$⊢\Re \left(A\right)\in ℝ\to \left|{\mathrm{e}}^{\mathrm{i}\Re \left(A\right)}\right|=1$$
36	4 35	syl	$$⊢A\in ℂ\to \left|{\mathrm{e}}^{\mathrm{i}\Re \left(A\right)}\right|=1$$
37	24	reefcld	$$⊢A\in ℂ\to {\mathrm{e}}^{-\Im \left(A\right)}\in ℝ$$
38		efgt0	$$⊢-\Im \left(A\right)\in ℝ\to 0<{\mathrm{e}}^{-\Im \left(A\right)}$$
39	24 38	syl	$$⊢A\in ℂ\to 0<{\mathrm{e}}^{-\Im \left(A\right)}$$
40		0re	$$⊢0\in ℝ$$
41		ltle	$$⊢\left(0\in ℝ\wedge {\mathrm{e}}^{-\Im \left(A\right)}\in ℝ\right)\to \left(0<{\mathrm{e}}^{-\Im \left(A\right)}\to 0\le {\mathrm{e}}^{-\Im \left(A\right)}\right)$$
42	40 41	mpan	$$⊢{\mathrm{e}}^{-\Im \left(A\right)}\in ℝ\to \left(0<{\mathrm{e}}^{-\Im \left(A\right)}\to 0\le {\mathrm{e}}^{-\Im \left(A\right)}\right)$$
43	37 39 42	sylc	$$⊢A\in ℂ\to 0\le {\mathrm{e}}^{-\Im \left(A\right)}$$
44	37 43	absidd	$$⊢A\in ℂ\to \left|{\mathrm{e}}^{-\Im \left(A\right)}\right|={\mathrm{e}}^{-\Im \left(A\right)}$$
45	36 44	oveq12d	$$⊢A\in ℂ\to \left|{\mathrm{e}}^{\mathrm{i}\Re \left(A\right)}\right|\left|{\mathrm{e}}^{-\Im \left(A\right)}\right|=1{\mathrm{e}}^{-\Im \left(A\right)}$$
46	33	mullidd	$$⊢A\in ℂ\to 1{\mathrm{e}}^{-\Im \left(A\right)}={\mathrm{e}}^{-\Im \left(A\right)}$$
47	34 45 46	3eqtrrd	$$⊢A\in ℂ\to {\mathrm{e}}^{-\Im \left(A\right)}=\left|{\mathrm{e}}^{\mathrm{i}\Re \left(A\right)}{\mathrm{e}}^{-\Im \left(A\right)}\right|$$
48		fveq2	$$⊢{\mathrm{e}}^{\mathrm{i}\Re \left(A\right)}{\mathrm{e}}^{-\Im \left(A\right)}=1\to \left|{\mathrm{e}}^{\mathrm{i}\Re \left(A\right)}{\mathrm{e}}^{-\Im \left(A\right)}\right|=\left|1\right|$$
49	47 48	sylan9eq	$$⊢\left(A\in ℂ\wedge {\mathrm{e}}^{\mathrm{i}\Re \left(A\right)}{\mathrm{e}}^{-\Im \left(A\right)}=1\right)\to {\mathrm{e}}^{-\Im \left(A\right)}=\left|1\right|$$
50	49	ex	$$⊢A\in ℂ\to \left({\mathrm{e}}^{\mathrm{i}\Re \left(A\right)}{\mathrm{e}}^{-\Im \left(A\right)}=1\to {\mathrm{e}}^{-\Im \left(A\right)}=\left|1\right|\right)$$
51	29 50	sylbid	$$⊢A\in ℂ\to \left({\mathrm{e}}^{\mathrm{i}A}=1\to {\mathrm{e}}^{-\Im \left(A\right)}=\left|1\right|\right)$$
52	7	negeq0d	$$⊢A\in ℂ\to \left(\Im \left(A\right)=0\leftrightarrow -\Im \left(A\right)=0\right)$$
53		reim0b	$$⊢A\in ℂ\to \left(A\in ℝ\leftrightarrow \Im \left(A\right)=0\right)$$
54		ef0	$$⊢{\mathrm{e}}^0=1$$
55		abs1	$$⊢\left|1\right|=1$$
56	54 55	eqtr4i	$$⊢{\mathrm{e}}^0=\left|1\right|$$
57	56	eqeq2i	$$⊢{\mathrm{e}}^{-\Im \left(A\right)}={\mathrm{e}}^0\leftrightarrow {\mathrm{e}}^{-\Im \left(A\right)}=\left|1\right|$$
58		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)$$
59	24 40 58	sylancl	$$⊢A\in ℂ\to \left({\mathrm{e}}^{-\Im \left(A\right)}={\mathrm{e}}^0\leftrightarrow -\Im \left(A\right)=0\right)$$
60	57 59	bitr3id	$$⊢A\in ℂ\to \left({\mathrm{e}}^{-\Im \left(A\right)}=\left|1\right|\leftrightarrow -\Im \left(A\right)=0\right)$$
61	52 53 60	3bitr4rd	$$⊢A\in ℂ\to \left({\mathrm{e}}^{-\Im \left(A\right)}=\left|1\right|\leftrightarrow A\in ℝ\right)$$
62	51 61	sylibd	$$⊢A\in ℂ\to \left({\mathrm{e}}^{\mathrm{i}A}=1\to A\in ℝ\right)$$
63	62	imp	$$⊢\left(A\in ℂ\wedge {\mathrm{e}}^{\mathrm{i}A}=1\right)\to A\in ℝ$$