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({\exp \upharpoonright }_{\mathrm{ran}log}\right):\mathrm{ran}log\underset{1-1\; onto}{⟶}ℂ\setminus \left\{0\right\}$$
2		f1ocnv	$$⊢\left({\exp \upharpoonright }_{\mathrm{ran}log}\right):\mathrm{ran}log\underset{1-1\; onto}{⟶}ℂ\setminus \left\{0\right\}\to {\left({\exp \upharpoonright }_{\mathrm{ran}log}\right)}^{-1}:ℂ\setminus \left\{0\right\}\underset{1-1\; onto}{⟶}\mathrm{ran}log$$
3	1 2	ax-mp	$$⊢{\left({\exp \upharpoonright }_{\mathrm{ran}log}\right)}^{-1}:ℂ\setminus \left\{0\right\}\underset{1-1\; onto}{⟶}\mathrm{ran}log$$
4		dflog2	$$⊢log={\left({\exp \upharpoonright }_{\mathrm{ran}log}\right)}^{-1}$$
5		f1oeq1	$$⊢log={\left({\exp \upharpoonright }_{\mathrm{ran}log}\right)}^{-1}\to \left(log:ℂ\setminus \left\{0\right\}\underset{1-1\; onto}{⟶}\mathrm{ran}log\leftrightarrow {\left({\exp \upharpoonright }_{\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\leftrightarrow {\left({\exp \upharpoonright }_{\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$$