Metamath Proof Explorer


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 AAeiA=1

Proof

Step Hyp Ref Expression
1 ef0 e0=1
2 1 eqeq2i eA=e0eA=1
3 imcl AA
4 3 renegcld AA
5 0re 0
6 reef11 A0eA=e0A=0
7 4 5 6 sylancl AeA=e0A=0
8 2 7 bitr3id AeA=1A=0
9 3 recnd AA
10 9 negeq0d AA=0A=0
11 8 10 bitr4d AeA=1A=0
12 ax-icn i
13 mulcl iAiA
14 12 13 mpan AiA
15 absef iAeiA=eiA
16 14 15 syl AeiA=eiA
17 recl AA
18 17 recnd AA
19 mulcl iAiA
20 12 9 19 sylancr AiA
21 replim AA=A+iA
22 18 20 21 comraddd AA=iA+A
23 22 oveq2d AiA=iiA+A
24 adddi iiAAiiA+A=iiA+iA
25 12 20 18 24 mp3an2i AiiA+A=iiA+iA
26 ixi ii=1
27 26 oveq1i iiA=-1A
28 mulass iiAiiA=iiA
29 12 12 9 28 mp3an12i AiiA=iiA
30 9 mulm1d A-1A=A
31 27 29 30 3eqtr3a AiiA=A
32 31 oveq1d AiiA+iA=-A+iA
33 25 32 eqtrd AiiA+A=-A+iA
34 23 33 eqtrd AiA=-A+iA
35 34 fveq2d AiA=-A+iA
36 4 17 crred A-A+iA=A
37 35 36 eqtrd AiA=A
38 37 fveq2d AeiA=eA
39 16 38 eqtrd AeiA=eA
40 39 eqeq1d AeiA=1eA=1
41 reim0b AAA=0
42 11 40 41 3bitr4rd AAeiA=1