# Metamath Proof Explorer

## Theorem logcnlem2

Description: Lemma for logcn . (Contributed by Mario Carneiro, 25-Feb-2015)

Ref Expression
Hypotheses logcn.d $⊢ D = ℂ ∖ −∞ 0$
logcnlem.s $⊢ S = if A ∈ ℝ + A ℑ ⁡ A$
logcnlem.t $⊢ T = A ⁢ R 1 + R$
logcnlem.a $⊢ φ → A ∈ D$
logcnlem.r $⊢ φ → R ∈ ℝ +$
Assertion logcnlem2 $⊢ φ → if S ≤ T S T ∈ ℝ +$

### Proof

Step Hyp Ref Expression
1 logcn.d $⊢ D = ℂ ∖ −∞ 0$
2 logcnlem.s $⊢ S = if A ∈ ℝ + A ℑ ⁡ A$
3 logcnlem.t $⊢ T = A ⁢ R 1 + R$
4 logcnlem.a $⊢ φ → A ∈ D$
5 logcnlem.r $⊢ φ → R ∈ ℝ +$
6 simpr $⊢ φ ∧ A ∈ ℝ + → A ∈ ℝ +$
7 1 ellogdm $⊢ A ∈ D ↔ A ∈ ℂ ∧ A ∈ ℝ → A ∈ ℝ +$
8 7 simplbi $⊢ A ∈ D → A ∈ ℂ$
9 4 8 syl $⊢ φ → A ∈ ℂ$
10 9 imcld $⊢ φ → ℑ ⁡ A ∈ ℝ$
11 10 adantr $⊢ φ ∧ ¬ A ∈ ℝ + → ℑ ⁡ A ∈ ℝ$
12 11 recnd $⊢ φ ∧ ¬ A ∈ ℝ + → ℑ ⁡ A ∈ ℂ$
13 reim0b $⊢ A ∈ ℂ → A ∈ ℝ ↔ ℑ ⁡ A = 0$
14 9 13 syl $⊢ φ → A ∈ ℝ ↔ ℑ ⁡ A = 0$
15 7 simprbi $⊢ A ∈ D → A ∈ ℝ → A ∈ ℝ +$
16 4 15 syl $⊢ φ → A ∈ ℝ → A ∈ ℝ +$
17 14 16 sylbird $⊢ φ → ℑ ⁡ A = 0 → A ∈ ℝ +$
18 17 necon3bd $⊢ φ → ¬ A ∈ ℝ + → ℑ ⁡ A ≠ 0$
19 18 imp $⊢ φ ∧ ¬ A ∈ ℝ + → ℑ ⁡ A ≠ 0$
20 12 19 absrpcld $⊢ φ ∧ ¬ A ∈ ℝ + → ℑ ⁡ A ∈ ℝ +$
21 6 20 ifclda $⊢ φ → if A ∈ ℝ + A ℑ ⁡ A ∈ ℝ +$
22 2 21 eqeltrid $⊢ φ → S ∈ ℝ +$
23 1 logdmn0 $⊢ A ∈ D → A ≠ 0$
24 4 23 syl $⊢ φ → A ≠ 0$
25 9 24 absrpcld $⊢ φ → A ∈ ℝ +$
26 1rp $⊢ 1 ∈ ℝ +$
27 rpaddcl $⊢ 1 ∈ ℝ + ∧ R ∈ ℝ + → 1 + R ∈ ℝ +$
28 26 5 27 sylancr $⊢ φ → 1 + R ∈ ℝ +$
29 5 28 rpdivcld $⊢ φ → R 1 + R ∈ ℝ +$
30 25 29 rpmulcld $⊢ φ → A ⁢ R 1 + R ∈ ℝ +$
31 3 30 eqeltrid $⊢ φ → T ∈ ℝ +$
32 22 31 ifcld $⊢ φ → if S ≤ T S T ∈ ℝ +$