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 A A e i A = 1

Proof

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