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