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. CC /\ ( exp ` ( _i x. A ) ) = 1 ) -> A e. RR )

Proof

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