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 = ( `' Im " ( -u _pi (,] _pi ) )

Proof

Step Hyp Ref Expression
1 df-log 
 |-  log = `' ( exp |` ( `' Im " ( -u _pi (,] _pi ) ) )
2 1 rneqi 
 |-  ran log = ran `' ( exp |` ( `' Im " ( -u _pi (,] _pi ) ) )
3 eqid 
 |-  ( `' Im " ( -u _pi (,] _pi ) ) = ( `' Im " ( -u _pi (,] _pi ) )
4 3 eff1o 
 |-  ( exp |` ( `' Im " ( -u _pi (,] _pi ) ) ) : ( `' Im " ( -u _pi (,] _pi ) ) -1-1-onto-> ( CC \ { 0 } )
5 f1ocnv 
 |-  ( ( exp |` ( `' Im " ( -u _pi (,] _pi ) ) ) : ( `' Im " ( -u _pi (,] _pi ) ) -1-1-onto-> ( CC \ { 0 } ) -> `' ( exp |` ( `' Im " ( -u _pi (,] _pi ) ) ) : ( CC \ { 0 } ) -1-1-onto-> ( `' Im " ( -u _pi (,] _pi ) ) )
6 4 5 ax-mp 
 |-  `' ( exp |` ( `' Im " ( -u _pi (,] _pi ) ) ) : ( CC \ { 0 } ) -1-1-onto-> ( `' Im " ( -u _pi (,] _pi ) )
7 f1ofo 
 |-  ( `' ( exp |` ( `' Im " ( -u _pi (,] _pi ) ) ) : ( CC \ { 0 } ) -1-1-onto-> ( `' Im " ( -u _pi (,] _pi ) ) -> `' ( exp |` ( `' Im " ( -u _pi (,] _pi ) ) ) : ( CC \ { 0 } ) -onto-> ( `' Im " ( -u _pi (,] _pi ) ) )
8 forn 
 |-  ( `' ( exp |` ( `' Im " ( -u _pi (,] _pi ) ) ) : ( CC \ { 0 } ) -onto-> ( `' Im " ( -u _pi (,] _pi ) ) -> ran `' ( exp |` ( `' Im " ( -u _pi (,] _pi ) ) ) = ( `' Im " ( -u _pi (,] _pi ) ) )
9 6 7 8 mp2b 
 |-  ran `' ( exp |` ( `' Im " ( -u _pi (,] _pi ) ) ) = ( `' Im " ( -u _pi (,] _pi ) )
10 2 9 eqtri 
 |-  ran log = ( `' Im " ( -u _pi (,] _pi ) )