# Metamath Proof Explorer

## Theorem logrn

Description: The range of the natural logarithm function, also the principal domain of the exponential function. This allows us 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({\mathrm{exp}↾}_{{\Im }^{-1}\left[\left(-\mathrm{\pi },\mathrm{\pi }\right]\right]}\right)}^{-1}$
2 1 rneqi ${⊢}\mathrm{ran}log=\mathrm{ran}{\left({\mathrm{exp}↾}_{{\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({\mathrm{exp}↾}_{{\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({\mathrm{exp}↾}_{{\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({\mathrm{exp}↾}_{{\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({\mathrm{exp}↾}_{{\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({\mathrm{exp}↾}_{{\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({\mathrm{exp}↾}_{{\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({\mathrm{exp}↾}_{{\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({\mathrm{exp}↾}_{{\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({\mathrm{exp}↾}_{{\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]$