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:ℂ\setminus \left\{0\right\}\underset{1-1 onto}{⟶}\mathrm{ran}log$

Proof

Step Hyp Ref Expression
1 eff1o2 ${⊢}\left({\mathrm{exp}↾}_{\mathrm{ran}log}\right):\mathrm{ran}log\underset{1-1 onto}{⟶}ℂ\setminus \left\{0\right\}$
2 f1ocnv ${⊢}\left({\mathrm{exp}↾}_{\mathrm{ran}log}\right):\mathrm{ran}log\underset{1-1 onto}{⟶}ℂ\setminus \left\{0\right\}\to {\left({\mathrm{exp}↾}_{\mathrm{ran}log}\right)}^{-1}:ℂ\setminus \left\{0\right\}\underset{1-1 onto}{⟶}\mathrm{ran}log$
3 1 2 ax-mp ${⊢}{\left({\mathrm{exp}↾}_{\mathrm{ran}log}\right)}^{-1}:ℂ\setminus \left\{0\right\}\underset{1-1 onto}{⟶}\mathrm{ran}log$
4 dflog2 ${⊢}log={\left({\mathrm{exp}↾}_{\mathrm{ran}log}\right)}^{-1}$
5 f1oeq1 ${⊢}log={\left({\mathrm{exp}↾}_{\mathrm{ran}log}\right)}^{-1}\to \left(log:ℂ\setminus \left\{0\right\}\underset{1-1 onto}{⟶}\mathrm{ran}log↔{\left({\mathrm{exp}↾}_{\mathrm{ran}log}\right)}^{-1}:ℂ\setminus \left\{0\right\}\underset{1-1 onto}{⟶}\mathrm{ran}log\right)$
6 4 5 ax-mp ${⊢}log:ℂ\setminus \left\{0\right\}\underset{1-1 onto}{⟶}\mathrm{ran}log↔{\left({\mathrm{exp}↾}_{\mathrm{ran}log}\right)}^{-1}:ℂ\setminus \left\{0\right\}\underset{1-1 onto}{⟶}\mathrm{ran}log$
7 3 6 mpbir ${⊢}log:ℂ\setminus \left\{0\right\}\underset{1-1 onto}{⟶}\mathrm{ran}log$