Metamath Proof Explorer

Theorem efifo

Description: The exponential function of an imaginary number maps the reals onto the unit circle. (Contributed by Mario Carneiro, 13-May-2014)

Ref Expression
Hypotheses efifo.1 
|- F = ( z e. RR |-> ( exp ` ( _i x. z ) ) )
efifo.2 
|- C = ( `' abs " { 1 } )
Assertion efifo 
|- F : RR -onto-> C

Proof

Step Hyp Ref Expression
1 efifo.1 
 |-  F = ( z e. RR |-> ( exp ` ( _i x. z ) ) )
2 efifo.2 
 |-  C = ( `' abs " { 1 } )
3 ax-icn 
 |-  _i e. CC
4 recn 
 |-  ( z e. RR -> z e. CC )
5 mulcl 
 |-  ( ( _i e. CC /\ z e. CC ) -> ( _i x. z ) e. CC )
6 3 4 5 sylancr 
 |-  ( z e. RR -> ( _i x. z ) e. CC )
7 efcl 
 |-  ( ( _i x. z ) e. CC -> ( exp ` ( _i x. z ) ) e. CC )
8 6 7 syl 
 |-  ( z e. RR -> ( exp ` ( _i x. z ) ) e. CC )
9 absefi 
 |-  ( z e. RR -> ( abs ` ( exp ` ( _i x. z ) ) ) = 1 )
10 absf 
 |-  abs : CC --> RR
11 ffn 
 |-  ( abs : CC --> RR -> abs Fn CC )
12 fniniseg 
 |-  ( abs Fn CC -> ( ( exp ` ( _i x. z ) ) e. ( `' abs " { 1 } ) <-> ( ( exp ` ( _i x. z ) ) e. CC /\ ( abs ` ( exp ` ( _i x. z ) ) ) = 1 ) ) )
13 10 11 12 mp2b 
 |-  ( ( exp ` ( _i x. z ) ) e. ( `' abs " { 1 } ) <-> ( ( exp ` ( _i x. z ) ) e. CC /\ ( abs ` ( exp ` ( _i x. z ) ) ) = 1 ) )
14 8 9 13 sylanbrc 
 |-  ( z e. RR -> ( exp ` ( _i x. z ) ) e. ( `' abs " { 1 } ) )
15 14 2 eleqtrrdi 
 |-  ( z e. RR -> ( exp ` ( _i x. z ) ) e. C )
16 1 15 fmpti 
 |-  F : RR --> C
17 ffn 
 |-  ( F : RR --> C -> F Fn RR )
18 16 17 ax-mp 
 |-  F Fn RR
19 frn 
 |-  ( F : RR --> C -> ran F C_ C )
20 16 19 ax-mp 
 |-  ran F C_ C
21 df-ima 
 |-  ( F " ( 0 (,] ( 2 x. _pi ) ) ) = ran ( F |` ( 0 (,] ( 2 x. _pi ) ) )
22 1 reseq1i 
 |-  ( F |` ( 0 (,] ( 2 x. _pi ) ) ) = ( ( z e. RR |-> ( exp ` ( _i x. z ) ) ) |` ( 0 (,] ( 2 x. _pi ) ) )
23 0xr 
 |-  0 e. RR*
24 2re 
 |-  2 e. RR
25 pire 
 |-  _pi e. RR
26 24 25 remulcli 
 |-  ( 2 x. _pi ) e. RR
27 elioc2 
 |-  ( ( 0 e. RR* /\ ( 2 x. _pi ) e. RR ) -> ( z e. ( 0 (,] ( 2 x. _pi ) ) <-> ( z e. RR /\ 0 < z /\ z <_ ( 2 x. _pi ) ) ) )
28 23 26 27 mp2an 
 |-  ( z e. ( 0 (,] ( 2 x. _pi ) ) <-> ( z e. RR /\ 0 < z /\ z <_ ( 2 x. _pi ) ) )
29 28 simp1bi 
 |-  ( z e. ( 0 (,] ( 2 x. _pi ) ) -> z e. RR )
30 29 ssriv 
 |-  ( 0 (,] ( 2 x. _pi ) ) C_ RR
31 resmpt 
 |-  ( ( 0 (,] ( 2 x. _pi ) ) C_ RR -> ( ( z e. RR |-> ( exp ` ( _i x. z ) ) ) |` ( 0 (,] ( 2 x. _pi ) ) ) = ( z e. ( 0 (,] ( 2 x. _pi ) ) |-> ( exp ` ( _i x. z ) ) ) )
32 30 31 ax-mp 
 |-  ( ( z e. RR |-> ( exp ` ( _i x. z ) ) ) |` ( 0 (,] ( 2 x. _pi ) ) ) = ( z e. ( 0 (,] ( 2 x. _pi ) ) |-> ( exp ` ( _i x. z ) ) )
33 22 32 eqtri 
 |-  ( F |` ( 0 (,] ( 2 x. _pi ) ) ) = ( z e. ( 0 (,] ( 2 x. _pi ) ) |-> ( exp ` ( _i x. z ) ) )
34 33 rneqi 
 |-  ran ( F |` ( 0 (,] ( 2 x. _pi ) ) ) = ran ( z e. ( 0 (,] ( 2 x. _pi ) ) |-> ( exp ` ( _i x. z ) ) )
35 0re 
 |-  0 e. RR
36 eqid 
 |-  ( z e. ( 0 (,] ( 2 x. _pi ) ) |-> ( exp ` ( _i x. z ) ) ) = ( z e. ( 0 (,] ( 2 x. _pi ) ) |-> ( exp ` ( _i x. z ) ) )
37 26 recni 
 |-  ( 2 x. _pi ) e. CC
38 37 addid2i 
 |-  ( 0 + ( 2 x. _pi ) ) = ( 2 x. _pi )
39 38 oveq2i 
 |-  ( 0 (,] ( 0 + ( 2 x. _pi ) ) ) = ( 0 (,] ( 2 x. _pi ) )
40 39 eqcomi 
 |-  ( 0 (,] ( 2 x. _pi ) ) = ( 0 (,] ( 0 + ( 2 x. _pi ) ) )
41 36 2 40 efif1o 
 |-  ( 0 e. RR -> ( z e. ( 0 (,] ( 2 x. _pi ) ) |-> ( exp ` ( _i x. z ) ) ) : ( 0 (,] ( 2 x. _pi ) ) -1-1-onto-> C )
42 35 41 ax-mp 
 |-  ( z e. ( 0 (,] ( 2 x. _pi ) ) |-> ( exp ` ( _i x. z ) ) ) : ( 0 (,] ( 2 x. _pi ) ) -1-1-onto-> C
43 f1ofo 
 |-  ( ( z e. ( 0 (,] ( 2 x. _pi ) ) |-> ( exp ` ( _i x. z ) ) ) : ( 0 (,] ( 2 x. _pi ) ) -1-1-onto-> C -> ( z e. ( 0 (,] ( 2 x. _pi ) ) |-> ( exp ` ( _i x. z ) ) ) : ( 0 (,] ( 2 x. _pi ) ) -onto-> C )
44 forn 
 |-  ( ( z e. ( 0 (,] ( 2 x. _pi ) ) |-> ( exp ` ( _i x. z ) ) ) : ( 0 (,] ( 2 x. _pi ) ) -onto-> C -> ran ( z e. ( 0 (,] ( 2 x. _pi ) ) |-> ( exp ` ( _i x. z ) ) ) = C )
45 42 43 44 mp2b 
 |-  ran ( z e. ( 0 (,] ( 2 x. _pi ) ) |-> ( exp ` ( _i x. z ) ) ) = C
46 34 45 eqtri 
 |-  ran ( F |` ( 0 (,] ( 2 x. _pi ) ) ) = C
47 21 46 eqtri 
 |-  ( F " ( 0 (,] ( 2 x. _pi ) ) ) = C
48 imassrn 
 |-  ( F " ( 0 (,] ( 2 x. _pi ) ) ) C_ ran F
49 47 48 eqsstrri 
 |-  C C_ ran F
50 20 49 eqssi 
 |-  ran F = C
51 df-fo 
 |-  ( F : RR -onto-> C <-> ( F Fn RR /\ ran F = C ) )
52 18 50 51 mpbir2an 
 |-  F : RR -onto-> C