Metamath Proof Explorer

Theorem logrnaddcl

Description: The range of the natural logarithm is closed under addition with reals. (Contributed by Mario Carneiro, 3-Apr-2015)

Ref Expression
Assertion logrnaddcl 
|- ( ( A e. ran log /\ B e. RR ) -> ( A + B ) e. ran log )

Proof

Step Hyp Ref Expression
1 logrncn 
 |-  ( A e. ran log -> A e. CC )
2 recn 
 |-  ( B e. RR -> B e. CC )
3 addcl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A + B ) e. CC )
4 1 2 3 syl2an 
 |-  ( ( A e. ran log /\ B e. RR ) -> ( A + B ) e. CC )
5 ellogrn 
 |-  ( A e. ran log <-> ( A e. CC /\ -u _pi < ( Im ` A ) /\ ( Im ` A ) <_ _pi ) )
6 5 simp2bi 
 |-  ( A e. ran log -> -u _pi < ( Im ` A ) )
7 6 adantr 
 |-  ( ( A e. ran log /\ B e. RR ) -> -u _pi < ( Im ` A ) )
8 imadd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( Im ` ( A + B ) ) = ( ( Im ` A ) + ( Im ` B ) ) )
9 1 2 8 syl2an 
 |-  ( ( A e. ran log /\ B e. RR ) -> ( Im ` ( A + B ) ) = ( ( Im ` A ) + ( Im ` B ) ) )
10 reim0 
 |-  ( B e. RR -> ( Im ` B ) = 0 )
11 10 adantl 
 |-  ( ( A e. ran log /\ B e. RR ) -> ( Im ` B ) = 0 )
12 11 oveq2d 
 |-  ( ( A e. ran log /\ B e. RR ) -> ( ( Im ` A ) + ( Im ` B ) ) = ( ( Im ` A ) + 0 ) )
13 1 adantr 
 |-  ( ( A e. ran log /\ B e. RR ) -> A e. CC )
14 13 imcld 
 |-  ( ( A e. ran log /\ B e. RR ) -> ( Im ` A ) e. RR )
15 14 recnd 
 |-  ( ( A e. ran log /\ B e. RR ) -> ( Im ` A ) e. CC )
16 15 addid1d 
 |-  ( ( A e. ran log /\ B e. RR ) -> ( ( Im ` A ) + 0 ) = ( Im ` A ) )
17 9 12 16 3eqtrd 
 |-  ( ( A e. ran log /\ B e. RR ) -> ( Im ` ( A + B ) ) = ( Im ` A ) )
18 7 17 breqtrrd 
 |-  ( ( A e. ran log /\ B e. RR ) -> -u _pi < ( Im ` ( A + B ) ) )
19 5 simp3bi 
 |-  ( A e. ran log -> ( Im ` A ) <_ _pi )
20 19 adantr 
 |-  ( ( A e. ran log /\ B e. RR ) -> ( Im ` A ) <_ _pi )
21 17 20 eqbrtrd 
 |-  ( ( A e. ran log /\ B e. RR ) -> ( Im ` ( A + B ) ) <_ _pi )
22 ellogrn 
 |-  ( ( A + B ) e. ran log <-> ( ( A + B ) e. CC /\ -u _pi < ( Im ` ( A + B ) ) /\ ( Im ` ( A + B ) ) <_ _pi ) )
23 4 18 21 22 syl3anbrc 
 |-  ( ( A e. ran log /\ B e. RR ) -> ( A + B ) e. ran log )