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

Metamath Proof Explorer

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