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