Metamath Proof Explorer


Theorem logcnlem3

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+
logcnlem.b φBD
logcnlem.l φAB<ifSTST
Assertion logcnlem3 φπ<logBlogAlogBlogAπ

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 logcnlem.b φBD
7 logcnlem.l φAB<ifSTST
8 pire π
9 8 renegcli π
10 9 a1i φA<0π
11 1 ellogdm BDBBB+
12 11 simplbi BDB
13 6 12 syl φB
14 1 logdmn0 BDB0
15 6 14 syl φB0
16 13 15 logcld φlogB
17 16 imcld φlogB
18 17 adantr φA<0logB
19 1 ellogdm ADAAA+
20 19 simplbi ADA
21 4 20 syl φA
22 1 logdmn0 ADA0
23 4 22 syl φA0
24 21 23 logcld φlogA
25 24 imcld φlogA
26 17 25 resubcld φlogBlogA
27 26 adantr φA<0logBlogA
28 13 15 logimcld φπ<logBlogBπ
29 28 simpld φπ<logB
30 29 adantr φA<0π<logB
31 17 recnd φlogB
32 31 adantr φA<0logB
33 32 subid1d φA<0logB0=logB
34 25 adantr φA<0logA
35 0red φA<00
36 argimlt0 AA<0logAπ0
37 21 36 sylan φA<0logAπ0
38 eliooord logAπ0π<logAlogA<0
39 37 38 syl φA<0π<logAlogA<0
40 39 simprd φA<0logA<0
41 34 35 18 40 ltsub2dd φA<0logB0<logBlogA
42 33 41 eqbrtrrd φA<0logB<logBlogA
43 10 18 27 30 42 lttrd φA<0π<logBlogA
44 29 adantr φA=0π<logB
45 reim0b AAA=0
46 21 45 syl φAA=0
47 19 simprbi ADAA+
48 4 47 syl φAA+
49 46 48 sylbird φA=0A+
50 49 imp φA=0A+
51 50 relogcld φA=0logA
52 51 reim0d φA=0logA=0
53 52 oveq2d φA=0logBlogA=logB0
54 31 subid1d φlogB0=logB
55 54 adantr φA=0logB0=logB
56 53 55 eqtrd φA=0logBlogA=logB
57 44 56 breqtrrd φA=0π<logBlogA
58 9 a1i φ0<Aπ
59 25 renegcld φlogA
60 59 adantr φ0<AlogA
61 26 adantr φ0<AlogBlogA
62 argimgt0 A0<AlogA0π
63 21 62 sylan φ0<AlogA0π
64 eliooord logA0π0<logAlogA<π
65 63 64 syl φ0<A0<logAlogA<π
66 65 simprd φ0<AlogA<π
67 ltneg logAπlogA<ππ<logA
68 25 8 67 sylancl φlogA<ππ<logA
69 68 adantr φ0<AlogA<ππ<logA
70 66 69 mpbid φ0<Aπ<logA
71 df-neg logA=0logA
72 13 adantr φ0<AB
73 21 13 imsubd φAB=AB
74 73 adantr φ0<AAB=AB
75 21 13 subcld φAB
76 75 imcld φAB
77 76 adantr φ0<AAB
78 75 abscld φAB
79 78 adantr φ0<AAB
80 21 adantr φ0<AA
81 80 imcld φ0<AA
82 absimle ABABAB
83 75 82 syl φABAB
84 76 78 absled φABABABABABAB
85 83 84 mpbid φABABABAB
86 85 simprd φABAB
87 86 adantr φ0<AABAB
88 rpre A+A
89 88 adantl φA+A
90 21 imcld φA
91 90 recnd φA
92 91 abscld φA
93 92 adantr φ¬A+A
94 89 93 ifclda φifA+AA
95 2 94 eqeltrid φS
96 21 abscld φA
97 5 rpred φR
98 1rp 1+
99 rpaddcl 1+R+1+R+
100 98 5 99 sylancr φ1+R+
101 97 100 rerpdivcld φR1+R
102 96 101 remulcld φAR1+R
103 3 102 eqeltrid φT
104 95 103 ifcld φifSTST
105 min1 STifSTSTS
106 95 103 105 syl2anc φifSTSTS
107 78 104 95 7 106 ltletrd φAB<S
108 107 adantr φ0<AAB<S
109 gt0ne0 A0<AA0
110 90 109 sylan φ0<AA0
111 88 46 syl5ib φA+A=0
112 111 necon3ad φA0¬A+
113 112 imp φA0¬A+
114 iffalse ¬A+ifA+AA=A
115 2 114 eqtrid ¬A+S=A
116 113 115 syl φA0S=A
117 110 116 syldan φ0<AS=A
118 0re 0
119 ltle 0A0<A0A
120 118 90 119 sylancr φ0<A0A
121 120 imp φ0<A0A
122 81 121 absidd φ0<AA=A
123 117 122 eqtrd φ0<AS=A
124 108 123 breqtrd φ0<AAB<A
125 77 79 81 87 124 lelttrd φ0<AAB<A
126 74 125 eqbrtrrd φ0<AAB<A
127 91 adantr φ0<AA
128 127 subid1d φ0<AA0=A
129 126 128 breqtrrd φ0<AAB<A0
130 0red φ0
131 13 imcld φB
132 130 131 90 ltsub2d φ0<BAB<A0
133 132 adantr φ0<A0<BAB<A0
134 129 133 mpbird φ0<A0<B
135 argimgt0 B0<BlogB0π
136 72 134 135 syl2anc φ0<AlogB0π
137 eliooord logB0π0<logBlogB<π
138 136 137 syl φ0<A0<logBlogB<π
139 138 simpld φ0<A0<logB
140 130 17 25 ltsub1d φ0<logB0logA<logBlogA
141 140 adantr φ0<A0<logB0logA<logBlogA
142 139 141 mpbid φ0<A0logA<logBlogA
143 71 142 eqbrtrid φ0<AlogA<logBlogA
144 58 60 61 70 143 lttrd φ0<Aπ<logBlogA
145 lttri4 A0A<0A=00<A
146 90 118 145 sylancl φA<0A=00<A
147 43 57 144 146 mpjao3dan φπ<logBlogA
148 8 a1i φA<0π
149 34 renegcld φA<0logA
150 13 adantr φA<0B
151 91 adantr φA<0A
152 151 subid1d φA<0A0=A
153 90 adantr φA<0A
154 78 renegcld φAB
155 154 adantr φA<0AB
156 76 adantr φA<0AB
157 78 adantr φA<0AB
158 107 adantr φA<0AB<S
159 118 ltnri ¬0<0
160 breq1 A=0A<00<0
161 159 160 mtbiri A=0¬A<0
162 161 necon2ai A<0A0
163 162 116 sylan2 φA<0S=A
164 ltle A0A<0A0
165 90 118 164 sylancl φA<0A0
166 165 imp φA<0A0
167 153 166 absnidd φA<0A=A
168 163 167 eqtrd φA<0S=A
169 158 168 breqtrd φA<0AB<A
170 157 153 169 ltnegcon2d φA<0A<AB
171 85 simpld φABAB
172 171 adantr φA<0ABAB
173 153 155 156 170 172 ltletrd φA<0A<AB
174 73 adantr φA<0AB=AB
175 173 174 breqtrd φA<0A<AB
176 152 175 eqbrtrd φA<0A0<AB
177 150 imcld φA<0B
178 177 35 153 ltsub2d φA<0B<0A0<AB
179 176 178 mpbird φA<0B<0
180 argimlt0 BB<0logBπ0
181 150 179 180 syl2anc φA<0logBπ0
182 eliooord logBπ0π<logBlogB<0
183 181 182 syl φA<0π<logBlogB<0
184 183 simprd φA<0logB<0
185 18 35 34 184 ltsub1dd φA<0logBlogA<0logA
186 185 71 breqtrrdi φA<0logBlogA<logA
187 39 simpld φA<0π<logA
188 ltnegcon1 πlogAπ<logAlogA<π
189 8 34 188 sylancr φA<0π<logAlogA<π
190 187 189 mpbid φA<0logA<π
191 27 149 148 186 190 lttrd φA<0logBlogA<π
192 27 148 191 ltled φA<0logBlogAπ
193 28 simprd φlogBπ
194 193 adantr φA=0logBπ
195 56 194 eqbrtrd φA=0logBlogAπ
196 8 a1i φ0<Aπ
197 17 adantr φ0<AlogB
198 0red φ0<A0
199 25 adantr φ0<AlogA
200 65 simpld φ0<A0<logA
201 198 199 197 200 ltsub2dd φ0<AlogBlogA<logB0
202 31 adantr φ0<AlogB
203 202 subid1d φ0<AlogB0=logB
204 201 203 breqtrd φ0<AlogBlogA<logB
205 138 simprd φ0<AlogB<π
206 61 197 196 204 205 lttrd φ0<AlogBlogA<π
207 61 196 206 ltled φ0<AlogBlogAπ
208 192 195 207 146 mpjao3dan φlogBlogAπ
209 147 208 jca φπ<logBlogAlogBlogAπ