This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem efif1o

Description: The exponential function of an imaginary number maps any open-below, closed-above interval of length 2 _pi one-to-one onto the unit circle. (Contributed by Paul Chapman, 16-Mar-2008) (Revised by Mario Carneiro, 13-May-2014)

Ref Expression
Hypotheses efif1o.1 
|- F = ( w e. D |-> ( exp ` ( _i x. w ) ) )
efif1o.2 
|- C = ( `' abs " { 1 } )
efif1o.3 
|- D = ( A (,] ( A + ( 2 x. _pi ) ) )
Assertion efif1o 
|- ( A e. RR -> F : D -1-1-onto-> C )

Proof

Step Hyp Ref Expression
1 efif1o.1 
 |-  F = ( w e. D |-> ( exp ` ( _i x. w ) ) )
2 efif1o.2 
 |-  C = ( `' abs " { 1 } )
3 efif1o.3 
 |-  D = ( A (,] ( A + ( 2 x. _pi ) ) )
4 rexr 
 |-  ( A e. RR -> A e. RR* )
5 2re 
 |-  2 e. RR
6 pire 
 |-  _pi e. RR
7 5 6 remulcli 
 |-  ( 2 x. _pi ) e. RR
8 readdcl 
 |-  ( ( A e. RR /\ ( 2 x. _pi ) e. RR ) -> ( A + ( 2 x. _pi ) ) e. RR )
9 7 8 mpan2 
 |-  ( A e. RR -> ( A + ( 2 x. _pi ) ) e. RR )
10 elioc2 
 |-  ( ( A e. RR* /\ ( A + ( 2 x. _pi ) ) e. RR ) -> ( x e. ( A (,] ( A + ( 2 x. _pi ) ) ) <-> ( x e. RR /\ A < x /\ x <_ ( A + ( 2 x. _pi ) ) ) ) )
11 4 9 10 syl2anc 
 |-  ( A e. RR -> ( x e. ( A (,] ( A + ( 2 x. _pi ) ) ) <-> ( x e. RR /\ A < x /\ x <_ ( A + ( 2 x. _pi ) ) ) ) )
12 simp1 
 |-  ( ( x e. RR /\ A < x /\ x <_ ( A + ( 2 x. _pi ) ) ) -> x e. RR )
13 11 12 biimtrdi 
 |-  ( A e. RR -> ( x e. ( A (,] ( A + ( 2 x. _pi ) ) ) -> x e. RR ) )
14 13 ssrdv 
 |-  ( A e. RR -> ( A (,] ( A + ( 2 x. _pi ) ) ) C_ RR )
15 3 14 eqsstrid 
 |-  ( A e. RR -> D C_ RR )
16 3 efif1olem1 
 |-  ( ( A e. RR /\ ( x e. D /\ y e. D ) ) -> ( abs ` ( x - y ) ) < ( 2 x. _pi ) )
17 3 efif1olem2 
 |-  ( ( A e. RR /\ z e. RR ) -> E. y e. D ( ( z - y ) / ( 2 x. _pi ) ) e. ZZ )
18 eqid 
 |-  ( sin |` ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) ) = ( sin |` ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) )
19 1 2 15 16 17 18 efif1olem4 
 |-  ( A e. RR -> F : D -1-1-onto-> C )