Theorem logcnlem2

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

	Ref	Expression
Hypotheses	logcn.d	$$⊢D=ℂ\setminus \left(\mathrm{-\infty },0\right]$$
	logcnlem.s	$$⊢S=if\left(A\in {ℝ}^{+},A,\left|\Im \left(A\right)\right|\right)$$
	logcnlem.t	$$⊢T=\left|A\right|\left(\frac{R}{1+R}\right)$$
	logcnlem.a	$$⊢\phi \to A\in D$$
	logcnlem.r	$$⊢\phi \to R\in {ℝ}^{+}$$
Assertion	logcnlem2	$$⊢\phi \to if\left(S\le T,S,T\right)\in {ℝ}^{+}$$

Proof

Step	Hyp	Ref	Expression
1		logcn.d	$$⊢D=ℂ\setminus \left(\mathrm{-\infty },0\right]$$
2		logcnlem.s	$$⊢S=if\left(A\in {ℝ}^{+},A,\left|\Im \left(A\right)\right|\right)$$
3		logcnlem.t	$$⊢T=\left|A\right|\left(\frac{R}{1+R}\right)$$
4		logcnlem.a	$$⊢\phi \to A\in D$$
5		logcnlem.r	$$⊢\phi \to R\in {ℝ}^{+}$$
6		simpr	$$⊢\left(\phi \wedge A\in {ℝ}^{+}\right)\to A\in {ℝ}^{+}$$
7	1	ellogdm	$$⊢A\in D\leftrightarrow \left(A\in ℂ\wedge \left(A\in ℝ\to A\in {ℝ}^{+}\right)\right)$$
8	7	simplbi	$$⊢A\in D\to A\in ℂ$$
9	4 8	syl	$$⊢\phi \to A\in ℂ$$
10	9	imcld	$$⊢\phi \to \Im \left(A\right)\in ℝ$$
11	10	adantr	$$⊢\left(\phi \wedge \neg A\in {ℝ}^{+}\right)\to \Im \left(A\right)\in ℝ$$
12	11	recnd	$$⊢\left(\phi \wedge \neg A\in {ℝ}^{+}\right)\to \Im \left(A\right)\in ℂ$$
13		reim0b	$$⊢A\in ℂ\to \left(A\in ℝ\leftrightarrow \Im \left(A\right)=0\right)$$
14	9 13	syl	$$⊢\phi \to \left(A\in ℝ\leftrightarrow \Im \left(A\right)=0\right)$$
15	7	simprbi	$$⊢A\in D\to \left(A\in ℝ\to A\in {ℝ}^{+}\right)$$
16	4 15	syl	$$⊢\phi \to \left(A\in ℝ\to A\in {ℝ}^{+}\right)$$
17	14 16	sylbird	$$⊢\phi \to \left(\Im \left(A\right)=0\to A\in {ℝ}^{+}\right)$$
18	17	necon3bd	$$⊢\phi \to \left(\neg A\in {ℝ}^{+}\to \Im \left(A\right)\ne 0\right)$$
19	18	imp	$$⊢\left(\phi \wedge \neg A\in {ℝ}^{+}\right)\to \Im \left(A\right)\ne 0$$
20	12 19	absrpcld	$$⊢\left(\phi \wedge \neg A\in {ℝ}^{+}\right)\to \left|\Im \left(A\right)\right|\in {ℝ}^{+}$$
21	6 20	ifclda	$$⊢\phi \to if\left(A\in {ℝ}^{+},A,\left|\Im \left(A\right)\right|\right)\in {ℝ}^{+}$$
22	2 21	eqeltrid	$$⊢\phi \to S\in {ℝ}^{+}$$
23	1	logdmn0	$$⊢A\in D\to A\ne 0$$
24	4 23	syl	$$⊢\phi \to A\ne 0$$
25	9 24	absrpcld	$$⊢\phi \to \left|A\right|\in {ℝ}^{+}$$
26		1rp	$$⊢1\in {ℝ}^{+}$$
27		rpaddcl	$$⊢\left(1\in {ℝ}^{+}\wedge R\in {ℝ}^{+}\right)\to 1+R\in {ℝ}^{+}$$
28	26 5 27	sylancr	$$⊢\phi \to 1+R\in {ℝ}^{+}$$
29	5 28	rpdivcld	$$⊢\phi \to \frac{R}{1+R}\in {ℝ}^{+}$$
30	25 29	rpmulcld	$$⊢\phi \to \left|A\right|\left(\frac{R}{1+R}\right)\in {ℝ}^{+}$$
31	3 30	eqeltrid	$$⊢\phi \to T\in {ℝ}^{+}$$
32	22 31	ifcld	$$⊢\phi \to if\left(S\le T,S,T\right)\in {ℝ}^{+}$$