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∈ran⁡log∧B∈ℝ→A+B∈ran⁡log

Proof

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