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