Metamath Proof Explorer


Theorem eff1o

Description: The exponential function maps the set S , of complex numbers with imaginary part in the closed-above, open-below interval from -upi to pi one-to-one onto the nonzero complex numbers. (Contributed by Paul Chapman, 16-Apr-2008) (Revised by Mario Carneiro, 13-May-2014)

Ref Expression
Hypothesis eff1o.1
|- S = ( `' Im " ( -u _pi (,] _pi ) )
Assertion eff1o
|- ( exp |` S ) : S -1-1-onto-> ( CC \ { 0 } )

Proof

Step Hyp Ref Expression
1 eff1o.1
 |-  S = ( `' Im " ( -u _pi (,] _pi ) )
2 pire
 |-  _pi e. RR
3 2 renegcli
 |-  -u _pi e. RR
4 eqid
 |-  ( w e. ( -u _pi (,] _pi ) |-> ( exp ` ( _i x. w ) ) ) = ( w e. ( -u _pi (,] _pi ) |-> ( exp ` ( _i x. w ) ) )
5 rexr
 |-  ( -u _pi e. RR -> -u _pi e. RR* )
6 iocssre
 |-  ( ( -u _pi e. RR* /\ _pi e. RR ) -> ( -u _pi (,] _pi ) C_ RR )
7 5 2 6 sylancl
 |-  ( -u _pi e. RR -> ( -u _pi (,] _pi ) C_ RR )
8 picn
 |-  _pi e. CC
9 8 2timesi
 |-  ( 2 x. _pi ) = ( _pi + _pi )
10 9 oveq2i
 |-  ( -u _pi + ( 2 x. _pi ) ) = ( -u _pi + ( _pi + _pi ) )
11 negpicn
 |-  -u _pi e. CC
12 8 8 addcli
 |-  ( _pi + _pi ) e. CC
13 11 12 addcomi
 |-  ( -u _pi + ( _pi + _pi ) ) = ( ( _pi + _pi ) + -u _pi )
14 12 8 negsubi
 |-  ( ( _pi + _pi ) + -u _pi ) = ( ( _pi + _pi ) - _pi )
15 8 8 pncan3oi
 |-  ( ( _pi + _pi ) - _pi ) = _pi
16 14 15 eqtri
 |-  ( ( _pi + _pi ) + -u _pi ) = _pi
17 10 13 16 3eqtrri
 |-  _pi = ( -u _pi + ( 2 x. _pi ) )
18 17 oveq2i
 |-  ( -u _pi (,] _pi ) = ( -u _pi (,] ( -u _pi + ( 2 x. _pi ) ) )
19 18 efif1olem1
 |-  ( ( -u _pi e. RR /\ ( x e. ( -u _pi (,] _pi ) /\ y e. ( -u _pi (,] _pi ) ) ) -> ( abs ` ( x - y ) ) < ( 2 x. _pi ) )
20 18 efif1olem2
 |-  ( ( -u _pi e. RR /\ z e. RR ) -> E. y e. ( -u _pi (,] _pi ) ( ( z - y ) / ( 2 x. _pi ) ) e. ZZ )
21 4 1 7 19 20 eff1olem
 |-  ( -u _pi e. RR -> ( exp |` S ) : S -1-1-onto-> ( CC \ { 0 } ) )
22 3 21 ax-mp
 |-  ( exp |` S ) : S -1-1-onto-> ( CC \ { 0 } )