Theorem eff1o2

Description: The exponential function restricted to its principal domain maps one-to-one onto the nonzero complex numbers. (Contributed by Paul Chapman, 21-Apr-2008) (Revised by Mario Carneiro, 13-May-2014)

	Ref	Expression
Assertion	eff1o2	$$⊢\left({\exp \upharpoonright }_{\mathrm{ran}log}\right):\mathrm{ran}log\underset{1-1\; onto}{⟶}ℂ\setminus \left\{0\right\}$$

Proof

Step	Hyp	Ref	Expression
1		logrn	$$⊢\mathrm{ran}log={\Im }^{-1}\left[\left(-\mathrm{\pi },\mathrm{\pi }\right]\right]$$
2	1	eff1o	$$⊢\left({\exp \upharpoonright }_{\mathrm{ran}log}\right):\mathrm{ran}log\underset{1-1\; onto}{⟶}ℂ\setminus \left\{0\right\}$$