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 ( ( 𝐴 ∈ ran log ∧ 𝐵 ∈ ℝ ) → ( 𝐴 + 𝐵 ) ∈ ran log )

Proof

Step Hyp Ref Expression
1 logrncn ⊢ ( 𝐴 ∈ ran log → 𝐴 ∈ ℂ )
2 recn ⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℂ )
3 addcl ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 + 𝐵 ) ∈ ℂ )
4 1 2 3 syl2an ⊢ ( ( 𝐴 ∈ ran log ∧ 𝐵 ∈ ℝ ) → ( 𝐴 + 𝐵 ) ∈ ℂ )
5 ellogrn ⊢ ( 𝐴 ∈ ran log ↔ ( 𝐴 ∈ ℂ ∧ - π < ( ℑ ‘ 𝐴 ) ∧ ( ℑ ‘ 𝐴 ) ≤ π ) )
6 5 simp2bi ⊢ ( 𝐴 ∈ ran log → - π < ( ℑ ‘ 𝐴 ) )
7 6 adantr ⊢ ( ( 𝐴 ∈ ran log ∧ 𝐵 ∈ ℝ ) → - π < ( ℑ ‘ 𝐴 ) )
8 imadd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ℑ ‘ ( 𝐴 + 𝐵 ) ) = ( ( ℑ ‘ 𝐴 ) + ( ℑ ‘ 𝐵 ) ) )
9 1 2 8 syl2an ⊢ ( ( 𝐴 ∈ ran log ∧ 𝐵 ∈ ℝ ) → ( ℑ ‘ ( 𝐴 + 𝐵 ) ) = ( ( ℑ ‘ 𝐴 ) + ( ℑ ‘ 𝐵 ) ) )
10 reim0 ⊢ ( 𝐵 ∈ ℝ → ( ℑ ‘ 𝐵 ) = 0 )
11 10 adantl ⊢ ( ( 𝐴 ∈ ran log ∧ 𝐵 ∈ ℝ ) → ( ℑ ‘ 𝐵 ) = 0 )
12 11 oveq2d ⊢ ( ( 𝐴 ∈ ran log ∧ 𝐵 ∈ ℝ ) → ( ( ℑ ‘ 𝐴 ) + ( ℑ ‘ 𝐵 ) ) = ( ( ℑ ‘ 𝐴 ) + 0 ) )
13 1 adantr ⊢ ( ( 𝐴 ∈ ran log ∧ 𝐵 ∈ ℝ ) → 𝐴 ∈ ℂ )
14 13 imcld ⊢ ( ( 𝐴 ∈ ran log ∧ 𝐵 ∈ ℝ ) → ( ℑ ‘ 𝐴 ) ∈ ℝ )
15 14 recnd ⊢ ( ( 𝐴 ∈ ran log ∧ 𝐵 ∈ ℝ ) → ( ℑ ‘ 𝐴 ) ∈ ℂ )
16 15 addid1d ⊢ ( ( 𝐴 ∈ ran log ∧ 𝐵 ∈ ℝ ) → ( ( ℑ ‘ 𝐴 ) + 0 ) = ( ℑ ‘ 𝐴 ) )
17 9 12 16 3eqtrd ⊢ ( ( 𝐴 ∈ ran log ∧ 𝐵 ∈ ℝ ) → ( ℑ ‘ ( 𝐴 + 𝐵 ) ) = ( ℑ ‘ 𝐴 ) )
18 7 17 breqtrrd ⊢ ( ( 𝐴 ∈ ran log ∧ 𝐵 ∈ ℝ ) → - π < ( ℑ ‘ ( 𝐴 + 𝐵 ) ) )
19 5 simp3bi ⊢ ( 𝐴 ∈ ran log → ( ℑ ‘ 𝐴 ) ≤ π )
20 19 adantr ⊢ ( ( 𝐴 ∈ ran log ∧ 𝐵 ∈ ℝ ) → ( ℑ ‘ 𝐴 ) ≤ π )
21 17 20 eqbrtrd ⊢ ( ( 𝐴 ∈ ran log ∧ 𝐵 ∈ ℝ ) → ( ℑ ‘ ( 𝐴 + 𝐵 ) ) ≤ π )
22 ellogrn ⊢ ( ( 𝐴 + 𝐵 ) ∈ ran log ↔ ( ( 𝐴 + 𝐵 ) ∈ ℂ ∧ - π < ( ℑ ‘ ( 𝐴 + 𝐵 ) ) ∧ ( ℑ ‘ ( 𝐴 + 𝐵 ) ) ≤ π ) )
23 4 18 21 22 syl3anbrc ⊢ ( ( 𝐴 ∈ ran log ∧ 𝐵 ∈ ℝ ) → ( 𝐴 + 𝐵 ) ∈ ran log )