This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ran ⁡ log = ℑ -1 − π π

Proof

Step Hyp Ref Expression
1 df-log ⊢ log = exp ↾ ℑ -1 − π π -1
2 1 rneqi ⊢ ran ⁡ log = ran ⁡ exp ↾ ℑ -1 − π π -1
3 eqid ⊢ ℑ -1 − π π = ℑ -1 − π π
4 3 eff1o ⊢ exp ↾ ℑ -1 − π π : ℑ -1 − π π ⟶ 1-1 onto ℂ ∖ 0
5 f1ocnv ⊢ exp ↾ ℑ -1 − π π : ℑ -1 − π π ⟶ 1-1 onto ℂ ∖ 0 → exp ↾ ℑ -1 − π π -1 : ℂ ∖ 0 ⟶ 1-1 onto ℑ -1 − π π
6 4 5 ax-mp ⊢ exp ↾ ℑ -1 − π π -1 : ℂ ∖ 0 ⟶ 1-1 onto ℑ -1 − π π
7 f1ofo ⊢ exp ↾ ℑ -1 − π π -1 : ℂ ∖ 0 ⟶ 1-1 onto ℑ -1 − π π → exp ↾ ℑ -1 − π π -1 : ℂ ∖ 0 ⟶ onto ℑ -1 − π π
8 forn ⊢ exp ↾ ℑ -1 − π π -1 : ℂ ∖ 0 ⟶ onto ℑ -1 − π π → ran ⁡ exp ↾ ℑ -1 − π π -1 = ℑ -1 − π π
9 6 7 8 mp2b ⊢ ran ⁡ exp ↾ ℑ -1 − π π -1 = ℑ -1 − π π
10 2 9 eqtri ⊢ ran ⁡ log = ℑ -1 − π π