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 = ( ◡ ℑ “ ( - π (,] π ) )

Proof

Step Hyp Ref Expression
1 df-log ⊢ log = ◡ ( exp ↾ ( ◡ ℑ “ ( - π (,] π ) ) )
2 1 rneqi ⊢ ran log = ran ◡ ( exp ↾ ( ◡ ℑ “ ( - π (,] π ) ) )
3 eqid ⊢ ( ◡ ℑ “ ( - π (,] π ) ) = ( ◡ ℑ “ ( - π (,] π ) )
4 3 eff1o ⊢ ( exp ↾ ( ◡ ℑ “ ( - π (,] π ) ) ) : ( ◡ ℑ “ ( - π (,] π ) ) –1-1-onto→ ( ℂ ∖ { 0 } )
5 f1ocnv ⊢ ( ( exp ↾ ( ◡ ℑ “ ( - π (,] π ) ) ) : ( ◡ ℑ “ ( - π (,] π ) ) –1-1-onto→ ( ℂ ∖ { 0 } ) → ◡ ( exp ↾ ( ◡ ℑ “ ( - π (,] π ) ) ) : ( ℂ ∖ { 0 } ) –1-1-onto→ ( ◡ ℑ “ ( - π (,] π ) ) )
6 4 5 ax-mp ⊢ ◡ ( exp ↾ ( ◡ ℑ “ ( - π (,] π ) ) ) : ( ℂ ∖ { 0 } ) –1-1-onto→ ( ◡ ℑ “ ( - π (,] π ) )
7 f1ofo ⊢ ( ◡ ( exp ↾ ( ◡ ℑ “ ( - π (,] π ) ) ) : ( ℂ ∖ { 0 } ) –1-1-onto→ ( ◡ ℑ “ ( - π (,] π ) ) → ◡ ( exp ↾ ( ◡ ℑ “ ( - π (,] π ) ) ) : ( ℂ ∖ { 0 } ) –onto→ ( ◡ ℑ “ ( - π (,] π ) ) )
8 forn ⊢ ( ◡ ( exp ↾ ( ◡ ℑ “ ( - π (,] π ) ) ) : ( ℂ ∖ { 0 } ) –onto→ ( ◡ ℑ “ ( - π (,] π ) ) → ran ◡ ( exp ↾ ( ◡ ℑ “ ( - π (,] π ) ) ) = ( ◡ ℑ “ ( - π (,] π ) ) )
9 6 7 8 mp2b ⊢ ran ◡ ( exp ↾ ( ◡ ℑ “ ( - π (,] π ) ) ) = ( ◡ ℑ “ ( - π (,] π ) )
10 2 9 eqtri ⊢ ran log = ( ◡ ℑ “ ( - π (,] π ) )