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 : ( ℂ ∖ { 0 } ) –1-1-onto→ ran log

Proof

Step Hyp Ref Expression
1 eff1o2 ⊢ ( exp ↾ ran log ) : ran log –1-1-onto→ ( ℂ ∖ { 0 } )
2 f1ocnv ⊢ ( ( exp ↾ ran log ) : ran log –1-1-onto→ ( ℂ ∖ { 0 } ) → ◡ ( exp ↾ ran log ) : ( ℂ ∖ { 0 } ) –1-1-onto→ ran log )
3 1 2 ax-mp ⊢ ◡ ( exp ↾ ran log ) : ( ℂ ∖ { 0 } ) –1-1-onto→ ran log
4 dflog2 ⊢ log = ◡ ( exp ↾ ran log )
5 f1oeq1 ⊢ ( log = ◡ ( exp ↾ ran log ) → ( log : ( ℂ ∖ { 0 } ) –1-1-onto→ ran log ↔ ◡ ( exp ↾ ran log ) : ( ℂ ∖ { 0 } ) –1-1-onto→ ran log ) )
6 4 5 ax-mp ⊢ ( log : ( ℂ ∖ { 0 } ) –1-1-onto→ ran log ↔ ◡ ( exp ↾ ran log ) : ( ℂ ∖ { 0 } ) –1-1-onto→ ran log )
7 3 6 mpbir ⊢ log : ( ℂ ∖ { 0 } ) –1-1-onto→ ran log