Theorem logrn

Description: The range of the natural logarithm function, also the principal domain of the exponential function. This allows to write the longer class expression as simply ran log . (Contributed by Paul Chapman, 21-Apr-2008) (Revised by Mario Carneiro, 13-May-2014)

	Ref	Expression
Assertion	logrn	$$⊢\mathrm{ran}log={\Im }^{-1}\left[\left(-\mathrm{\pi },\mathrm{\pi }\right]\right]$$

Proof

Step	Hyp	Ref	Expression
1		df-log	$$⊢log={\left({\exp \upharpoonright }_{{\Im }^{-1}\left[\left(-\mathrm{\pi },\mathrm{\pi }\right]\right]}\right)}^{-1}$$
2	1	rneqi	$$⊢\mathrm{ran}log=\mathrm{ran}{\left({\exp \upharpoonright }_{{\Im }^{-1}\left[\left(-\mathrm{\pi },\mathrm{\pi }\right]\right]}\right)}^{-1}$$
3		eqid	$$⊢{\Im }^{-1}\left[\left(-\mathrm{\pi },\mathrm{\pi }\right]\right]={\Im }^{-1}\left[\left(-\mathrm{\pi },\mathrm{\pi }\right]\right]$$
4	3	eff1o	$$⊢\left({\exp \upharpoonright }_{{\Im }^{-1}\left[\left(-\mathrm{\pi },\mathrm{\pi }\right]\right]}\right):{\Im }^{-1}\left[\left(-\mathrm{\pi },\mathrm{\pi }\right]\right]\underset{1-1\; onto}{⟶}ℂ\setminus \left\{0\right\}$$
5		f1ocnv	$$⊢\left({\exp \upharpoonright }_{{\Im }^{-1}\left[\left(-\mathrm{\pi },\mathrm{\pi }\right]\right]}\right):{\Im }^{-1}\left[\left(-\mathrm{\pi },\mathrm{\pi }\right]\right]\underset{1-1\; onto}{⟶}ℂ\setminus \left\{0\right\}\to {\left({\exp \upharpoonright }_{{\Im }^{-1}\left[\left(-\mathrm{\pi },\mathrm{\pi }\right]\right]}\right)}^{-1}:ℂ\setminus \left\{0\right\}\underset{1-1\; onto}{⟶}{\Im }^{-1}\left[\left(-\mathrm{\pi },\mathrm{\pi }\right]\right]$$
6	4 5	ax-mp	$$⊢{\left({\exp \upharpoonright }_{{\Im }^{-1}\left[\left(-\mathrm{\pi },\mathrm{\pi }\right]\right]}\right)}^{-1}:ℂ\setminus \left\{0\right\}\underset{1-1\; onto}{⟶}{\Im }^{-1}\left[\left(-\mathrm{\pi },\mathrm{\pi }\right]\right]$$
7		f1ofo	$$⊢{\left({\exp \upharpoonright }_{{\Im }^{-1}\left[\left(-\mathrm{\pi },\mathrm{\pi }\right]\right]}\right)}^{-1}:ℂ\setminus \left\{0\right\}\underset{1-1\; onto}{⟶}{\Im }^{-1}\left[\left(-\mathrm{\pi },\mathrm{\pi }\right]\right]\to {\left({\exp \upharpoonright }_{{\Im }^{-1}\left[\left(-\mathrm{\pi },\mathrm{\pi }\right]\right]}\right)}^{-1}:ℂ\setminus \left\{0\right\}\underset{onto}{⟶}{\Im }^{-1}\left[\left(-\mathrm{\pi },\mathrm{\pi }\right]\right]$$
8		forn	$$⊢{\left({\exp \upharpoonright }_{{\Im }^{-1}\left[\left(-\mathrm{\pi },\mathrm{\pi }\right]\right]}\right)}^{-1}:ℂ\setminus \left\{0\right\}\underset{onto}{⟶}{\Im }^{-1}\left[\left(-\mathrm{\pi },\mathrm{\pi }\right]\right]\to \mathrm{ran}{\left({\exp \upharpoonright }_{{\Im }^{-1}\left[\left(-\mathrm{\pi },\mathrm{\pi }\right]\right]}\right)}^{-1}={\Im }^{-1}\left[\left(-\mathrm{\pi },\mathrm{\pi }\right]\right]$$
9	6 7 8	mp2b	$$⊢\mathrm{ran}{\left({\exp \upharpoonright }_{{\Im }^{-1}\left[\left(-\mathrm{\pi },\mathrm{\pi }\right]\right]}\right)}^{-1}={\Im }^{-1}\left[\left(-\mathrm{\pi },\mathrm{\pi }\right]\right]$$
10	2 9	eqtri	$$⊢\mathrm{ran}log={\Im }^{-1}\left[\left(-\mathrm{\pi },\mathrm{\pi }\right]\right]$$