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