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

Metamath Proof Explorer

Theorem logf1o

Description: The natural logarithm function maps the nonzero complex numbers one-to-one onto its range. (Contributed by Paul Chapman, 21-Apr-2008)

Ref Expression
Assertion logf1o 
|- log : ( CC \ { 0 } ) -1-1-onto-> ran log

Proof

Step Hyp Ref Expression
1 eff1o2 
 |-  ( exp |` ran log ) : ran log -1-1-onto-> ( CC \ { 0 } )
2 f1ocnv 
 |-  ( ( exp |` ran log ) : ran log -1-1-onto-> ( CC \ { 0 } ) -> `' ( exp |` ran log ) : ( CC \ { 0 } ) -1-1-onto-> ran log )
3 1 2 ax-mp 
 |-  `' ( exp |` ran log ) : ( CC \ { 0 } ) -1-1-onto-> ran log
4 dflog2 
 |-  log = `' ( exp |` ran log )
5 f1oeq1 
 |-  ( log = `' ( exp |` ran log ) -> ( log : ( CC \ { 0 } ) -1-1-onto-> ran log <-> `' ( exp |` ran log ) : ( CC \ { 0 } ) -1-1-onto-> ran log ) )
6 4 5 ax-mp 
 |-  ( log : ( CC \ { 0 } ) -1-1-onto-> ran log <-> `' ( exp |` ran log ) : ( CC \ { 0 } ) -1-1-onto-> ran log )
7 3 6 mpbir 
 |-  log : ( CC \ { 0 } ) -1-1-onto-> ran log