Metamath Proof Explorer


Theorem efieq1re

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

Ref Expression
Assertion efieq1re A e i A = 1 A

Proof

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