This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem logcnlem2

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

Ref Expression
Hypotheses logcn.d ⊢ 𝐷 = ( ℂ ∖ ( -∞ (,] 0 ) )
logcnlem.s ⊢ 𝑆 = if ( 𝐴 ∈ ℝ+ , 𝐴 , ( abs ‘ ( ℑ ‘ 𝐴 ) ) )
logcnlem.t ⊢ 𝑇 = ( ( abs ‘ 𝐴 ) · ( 𝑅 / ( 1 + 𝑅 ) ) )
logcnlem.a ⊢ ( 𝜑 → 𝐴 ∈ 𝐷 )
logcnlem.r ⊢ ( 𝜑 → 𝑅 ∈ ℝ+ )
Assertion logcnlem2 ( 𝜑 → if ( 𝑆 ≤ 𝑇 , 𝑆 , 𝑇 ) ∈ ℝ+ )

Proof

Step Hyp Ref Expression
1 logcn.d ⊢ 𝐷 = ( ℂ ∖ ( -∞ (,] 0 ) )
2 logcnlem.s ⊢ 𝑆 = if ( 𝐴 ∈ ℝ+ , 𝐴 , ( abs ‘ ( ℑ ‘ 𝐴 ) ) )
3 logcnlem.t ⊢ 𝑇 = ( ( abs ‘ 𝐴 ) · ( 𝑅 / ( 1 + 𝑅 ) ) )
4 logcnlem.a ⊢ ( 𝜑 → 𝐴 ∈ 𝐷 )
5 logcnlem.r ⊢ ( 𝜑 → 𝑅 ∈ ℝ+ )
6 simpr ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℝ+ ) → 𝐴 ∈ ℝ+ )
7 1 ellogdm ⊢ ( 𝐴 ∈ 𝐷 ↔ ( 𝐴 ∈ ℂ ∧ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℝ+ ) ) )
8 7 simplbi ⊢ ( 𝐴 ∈ 𝐷 → 𝐴 ∈ ℂ )
9 4 8 syl ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
10 9 imcld ⊢ ( 𝜑 → ( ℑ ‘ 𝐴 ) ∈ ℝ )
11 10 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ ℝ+ ) → ( ℑ ‘ 𝐴 ) ∈ ℝ )
12 11 recnd ⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ ℝ+ ) → ( ℑ ‘ 𝐴 ) ∈ ℂ )
13 reim0b ⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ∈ ℝ ↔ ( ℑ ‘ 𝐴 ) = 0 ) )
14 9 13 syl ⊢ ( 𝜑 → ( 𝐴 ∈ ℝ ↔ ( ℑ ‘ 𝐴 ) = 0 ) )
15 7 simprbi ⊢ ( 𝐴 ∈ 𝐷 → ( 𝐴 ∈ ℝ → 𝐴 ∈ ℝ+ ) )
16 4 15 syl ⊢ ( 𝜑 → ( 𝐴 ∈ ℝ → 𝐴 ∈ ℝ+ ) )
17 14 16 sylbird ⊢ ( 𝜑 → ( ( ℑ ‘ 𝐴 ) = 0 → 𝐴 ∈ ℝ+ ) )
18 17 necon3bd ⊢ ( 𝜑 → ( ¬ 𝐴 ∈ ℝ+ → ( ℑ ‘ 𝐴 ) ≠ 0 ) )
19 18 imp ⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ ℝ+ ) → ( ℑ ‘ 𝐴 ) ≠ 0 )
20 12 19 absrpcld ⊢ ( ( 𝜑 ∧ ¬ 𝐴 ∈ ℝ+ ) → ( abs ‘ ( ℑ ‘ 𝐴 ) ) ∈ ℝ+ )
21 6 20 ifclda ⊢ ( 𝜑 → if ( 𝐴 ∈ ℝ+ , 𝐴 , ( abs ‘ ( ℑ ‘ 𝐴 ) ) ) ∈ ℝ+ )
22 2 21 eqeltrid ⊢ ( 𝜑 → 𝑆 ∈ ℝ+ )
23 1 logdmn0 ⊢ ( 𝐴 ∈ 𝐷 → 𝐴 ≠ 0 )
24 4 23 syl ⊢ ( 𝜑 → 𝐴 ≠ 0 )
25 9 24 absrpcld ⊢ ( 𝜑 → ( abs ‘ 𝐴 ) ∈ ℝ+ )
26 1rp ⊢ 1 ∈ ℝ+
27 rpaddcl ⊢ ( ( 1 ∈ ℝ+ ∧ 𝑅 ∈ ℝ+ ) → ( 1 + 𝑅 ) ∈ ℝ+ )
28 26 5 27 sylancr ⊢ ( 𝜑 → ( 1 + 𝑅 ) ∈ ℝ+ )
29 5 28 rpdivcld ⊢ ( 𝜑 → ( 𝑅 / ( 1 + 𝑅 ) ) ∈ ℝ+ )
30 25 29 rpmulcld ⊢ ( 𝜑 → ( ( abs ‘ 𝐴 ) · ( 𝑅 / ( 1 + 𝑅 ) ) ) ∈ ℝ+ )
31 3 30 eqeltrid ⊢ ( 𝜑 → 𝑇 ∈ ℝ+ )
32 22 31 ifcld ⊢ ( 𝜑 → if ( 𝑆 ≤ 𝑇 , 𝑆 , 𝑇 ) ∈ ℝ+ )