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