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=ifA+AA
logcnlem.t T=AR1+R
logcnlem.a φAD
logcnlem.r φR+
Assertion logcnlem2 φifSTST+

Proof

Step Hyp Ref Expression
1 logcn.d D=−∞0
2 logcnlem.s S=ifA+AA
3 logcnlem.t T=AR1+R
4 logcnlem.a φAD
5 logcnlem.r φR+
6 simpr φA+A+
7 1 ellogdm ADAAA+
8 7 simplbi ADA
9 4 8 syl φA
10 9 imcld φA
11 10 adantr φ¬A+A
12 11 recnd φ¬A+A
13 reim0b AAA=0
14 9 13 syl φAA=0
15 7 simprbi ADAA+
16 4 15 syl φAA+
17 14 16 sylbird φA=0A+
18 17 necon3bd φ¬A+A0
19 18 imp φ¬A+A0
20 12 19 absrpcld φ¬A+A+
21 6 20 ifclda φifA+AA+
22 2 21 eqeltrid φS+
23 1 logdmn0 ADA0
24 4 23 syl φA0
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 φR1+R+
30 25 29 rpmulcld φAR1+R+
31 3 30 eqeltrid φT+
32 22 31 ifcld φifSTST+