Metamath Proof Explorer

Theorem relogrn

Description: The range of the natural logarithm function includes the real numbers. (Contributed by Paul Chapman, 21-Apr-2008) (Proof shortened by Mario Carneiro, 1-Apr-2015)

Ref Expression
Assertion relogrn 
|- ( A e. RR -> A e. ran log )

Proof

Step Hyp Ref Expression
1 recn 
 |-  ( A e. RR -> A e. CC )
2 pipos 
 |-  0 < _pi
3 pire 
 |-  _pi e. RR
4 lt0neg2 
 |-  ( _pi e. RR -> ( 0 < _pi <-> -u _pi < 0 ) )
5 3 4 ax-mp 
 |-  ( 0 < _pi <-> -u _pi < 0 )
6 2 5 mpbi 
 |-  -u _pi < 0
7 reim0 
 |-  ( A e. RR -> ( Im ` A ) = 0 )
8 6 7 breqtrrid 
 |-  ( A e. RR -> -u _pi < ( Im ` A ) )
9 0re 
 |-  0 e. RR
10 9 3 2 ltleii 
 |-  0 <_ _pi
11 7 10 eqbrtrdi 
 |-  ( A e. RR -> ( Im ` A ) <_ _pi )
12 ellogrn 
 |-  ( A e. ran log <-> ( A e. CC /\ -u _pi < ( Im ` A ) /\ ( Im ` A ) <_ _pi ) )
13 1 8 11 12 syl3anbrc 
 |-  ( A e. RR -> A e. ran log )