Theorem eff2

Description: The exponential function maps the complex numbers to the nonzero complex numbers. (Contributed by Paul Chapman, 16-Apr-2008)

	Ref	Expression
Assertion	eff2	|- exp : CC --> ( CC \ { 0 } )

Proof

Step	Hyp	Ref	Expression
1		eff	|- exp : CC --> CC
2		ffn	|- ( exp : CC --> CC -> exp Fn CC )
3	1 2	ax-mp	|- exp Fn CC
4		efcl	|- ( x e. CC -> ( exp ` x ) e. CC )
5		efne0	|- ( x e. CC -> ( exp ` x ) =/= 0 )
6		eldifsn	|- ( ( exp ` x ) e. ( CC \ { 0 } ) <-> ( ( exp ` x ) e. CC /\ ( exp ` x ) =/= 0 ) )
7	4 5 6	sylanbrc	|- ( x e. CC -> ( exp ` x ) e. ( CC \ { 0 } ) )
8	7	rgen	|- A. x e. CC ( exp ` x ) e. ( CC \ { 0 } )
9		ffnfv	|- ( exp : CC --> ( CC \ { 0 } ) <-> ( exp Fn CC /\ A. x e. CC ( exp ` x ) e. ( CC \ { 0 } ) ) )
10	3 8 9	mpbir2an	|- exp : CC --> ( CC \ { 0 } )