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

Metamath Proof Explorer

Theorem eff1o

Proof