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 ( 𝑆 ≤ 𝑇 , 𝑆 , 𝑇 ) ∈ ℝ+ )