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 } )