Metamath Proof Explorer


Theorem logcnlem4

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 logcnlem4 φlogAlogB<R

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 1 ellogdm ADAAA+
9 8 simplbi ADA
10 4 9 syl φA
11 1 logdmn0 ADA0
12 4 11 syl φA0
13 10 12 logcld φlogA
14 13 imcld φlogA
15 14 recnd φlogA
16 1 ellogdm BDBBB+
17 16 simplbi BDB
18 6 17 syl φB
19 1 logdmn0 BDB0
20 6 19 syl φB0
21 18 20 logcld φlogB
22 21 imcld φlogB
23 22 recnd φlogB
24 15 23 abssubd φlogAlogB=logBlogA
25 21 13 imsubd φlogBlogA=logBlogA
26 efsub logBlogAelogBlogA=elogBelogA
27 21 13 26 syl2anc φelogBlogA=elogBelogA
28 eflog BB0elogB=B
29 18 20 28 syl2anc φelogB=B
30 eflog AA0elogA=A
31 10 12 30 syl2anc φelogA=A
32 29 31 oveq12d φelogBelogA=BA
33 27 32 eqtrd φelogBlogA=BA
34 18 10 12 divcld φBA
35 18 10 20 12 divne0d φBA0
36 21 13 subcld φlogBlogA
37 1 2 3 4 5 6 7 logcnlem3 φπ<logBlogAlogBlogAπ
38 37 simpld φπ<logBlogA
39 38 25 breqtrrd φπ<logBlogA
40 37 simprd φlogBlogAπ
41 25 40 eqbrtrd φlogBlogAπ
42 ellogrn logBlogAranloglogBlogAπ<logBlogAlogBlogAπ
43 36 39 41 42 syl3anbrc φlogBlogAranlog
44 logeftb BABA0logBlogAranloglogBA=logBlogAelogBlogA=BA
45 34 35 43 44 syl3anc φlogBA=logBlogAelogBlogA=BA
46 33 45 mpbird φlogBA=logBlogA
47 46 eqcomd φlogBlogA=logBA
48 47 fveq2d φlogBlogA=logBA
49 25 48 eqtr3d φlogBlogA=logBA
50 49 fveq2d φlogBlogA=logBA
51 24 50 eqtrd φlogAlogB=logBA
52 34 35 logcld φlogBA
53 52 imcld φlogBA
54 53 recnd φlogBA
55 54 abscld φlogBA
56 0red φ0
57 1re 1
58 10 18 subcld φAB
59 58 abscld φAB
60 10 12 absrpcld φA+
61 59 60 rerpdivcld φABA
62 resubcl 1ABA1ABA
63 57 61 62 sylancr φ1ABA
64 34 recld φBA
65 10 abscld φA
66 5 rpred φR
67 1rp 1+
68 rpaddcl 1+R+1+R+
69 67 5 68 sylancr φ1+R+
70 66 69 rerpdivcld φR1+R
71 65 70 remulcld φAR1+R
72 3 71 eqeltrid φT
73 rpre A+A
74 73 adantl φA+A
75 10 imcld φA
76 75 recnd φA
77 76 abscld φA
78 77 adantr φ¬A+A
79 74 78 ifclda φifA+AA
80 2 79 eqeltrid φS
81 ltmin ABSTAB<ifSTSTAB<SAB<T
82 59 80 72 81 syl3anc φAB<ifSTSTAB<SAB<T
83 7 82 mpbid φAB<SAB<T
84 83 simprd φAB<T
85 69 rpred φ1+R
86 66 ltp1d φR<R+1
87 66 recnd φR
88 ax-1cn 1
89 addcom R1R+1=1+R
90 87 88 89 sylancl φR+1=1+R
91 86 90 breqtrd φR<1+R
92 66 85 91 ltled φR1+R
93 85 recnd φ1+R
94 93 mulid1d φ1+R1=1+R
95 92 94 breqtrrd φR1+R1
96 57 a1i φ1
97 66 96 69 ledivmuld φR1+R1R1+R1
98 95 97 mpbird φR1+R1
99 70 96 60 lemul2d φR1+R1AR1+RA1
100 98 99 mpbid φAR1+RA1
101 65 recnd φA
102 101 mulid1d φA1=A
103 100 102 breqtrd φAR1+RA
104 3 103 eqbrtrid φTA
105 59 72 65 84 104 ltletrd φAB<A
106 105 102 breqtrrd φAB<A1
107 59 96 60 ltdivmuld φABA<1AB<A1
108 106 107 mpbird φABA<1
109 posdif ABA1ABA<10<1ABA
110 61 57 109 sylancl φABA<10<1ABA
111 108 110 mpbid φ0<1ABA
112 58 10 12 divcld φABA
113 112 releabsd φABAABA
114 10 18 10 12 divsubdird φABA=AABA
115 10 12 dividd φAA=1
116 115 oveq1d φAABA=1BA
117 114 116 eqtrd φABA=1BA
118 117 fveq2d φABA=1BA
119 resub 1BA1BA=1BA
120 88 34 119 sylancr φ1BA=1BA
121 118 120 eqtrd φABA=1BA
122 re1 1=1
123 122 oveq1i 1BA=1BA
124 121 123 eqtrdi φABA=1BA
125 58 10 12 absdivd φABA=ABA
126 113 124 125 3brtr3d φ1BAABA
127 96 64 61 126 subled φ1ABABA
128 56 63 64 111 127 ltletrd φ0<BA
129 argregt0 BA0<BAlogBAπ2π2
130 34 128 129 syl2anc φlogBAπ2π2
131 cosq14gt0 logBAπ2π20<coslogBA
132 130 131 syl φ0<coslogBA
133 132 gt0ne0d φcoslogBA0
134 53 133 retancld φtanlogBA
135 134 recnd φtanlogBA
136 135 abscld φtanlogBA
137 tanabsge logBAπ2π2logBAtanlogBA
138 130 137 syl φlogBAtanlogBA
139 128 gt0ne0d φBA0
140 tanarg BABA0tanlogBA=BABA
141 34 139 140 syl2anc φtanlogBA=BABA
142 141 fveq2d φtanlogBA=BABA
143 34 imcld φBA
144 143 recnd φBA
145 64 recnd φBA
146 144 145 139 absdivd φBABA=BABA
147 56 64 128 ltled φ0BA
148 64 147 absidd φBA=BA
149 148 oveq2d φBABA=BABA
150 142 146 149 3eqtrd φtanlogBA=BABA
151 144 abscld φBA
152 64 66 remulcld φBAR
153 18 10 subcld φBA
154 153 10 12 divcld φBAA
155 absimle BAABAABAA
156 154 155 syl φBAABAA
157 18 10 10 12 divsubdird φBAA=BAAA
158 115 oveq2d φBAAA=BA1
159 157 158 eqtrd φBAA=BA1
160 159 fveq2d φBAA=BA1
161 imsub BA1BA1=BA1
162 34 88 161 sylancl φBA1=BA1
163 im1 1=0
164 163 oveq2i BA1=BA0
165 162 164 eqtrdi φBA1=BA0
166 144 subid1d φBA0=BA
167 160 165 166 3eqtrrd φBA=BAA
168 167 fveq2d φBA=BAA
169 10 18 abssubd φAB=BA
170 169 oveq1d φABA=BAA
171 153 10 12 absdivd φBAA=BAA
172 170 171 eqtr4d φABA=BAA
173 156 168 172 3brtr4d φBAABA
174 65 59 resubcld φAAB
175 174 66 remulcld φAABR
176 65 152 remulcld φABAR
177 59 recnd φAB
178 88 a1i φ1
179 177 178 87 adddid φAB1+R=AB1+ABR
180 177 mulid1d φAB1=AB
181 180 oveq1d φAB1+ABR=AB+ABR
182 179 181 eqtrd φAB1+R=AB+ABR
183 69 rpne0d φ1+R0
184 101 87 93 183 divassd φAR1+R=AR1+R
185 184 3 eqtr4di φAR1+R=T
186 84 185 breqtrrd φAB<AR1+R
187 65 66 remulcld φAR
188 59 187 69 ltmuldivd φAB1+R<ARAB<AR1+R
189 186 188 mpbird φAB1+R<AR
190 182 189 eqbrtrrd φAB+ABR<AR
191 59 66 remulcld φABR
192 59 191 187 ltaddsubd φAB+ABR<ARAB<ARABR
193 190 192 mpbid φAB<ARABR
194 101 177 87 subdird φAABR=ARABR
195 193 194 breqtrrd φAB<AABR
196 60 rpne0d φA0
197 101 177 101 196 divsubdird φAABA=AAABA
198 101 196 dividd φAA=1
199 198 oveq1d φAAABA=1ABA
200 197 199 eqtrd φAABA=1ABA
201 200 127 eqbrtrd φAABABA
202 174 64 60 ledivmuld φAABABAAABABA
203 201 202 mpbid φAABABA
204 65 64 remulcld φABA
205 174 204 5 lemul1d φAABABAAABRABAR
206 203 205 mpbid φAABRABAR
207 101 145 87 mulassd φABAR=ABAR
208 206 207 breqtrd φAABRABAR
209 59 175 176 195 208 ltletrd φAB<ABAR
210 59 152 60 ltdivmuld φABA<BARAB<ABAR
211 209 210 mpbird φABA<BAR
212 151 61 152 173 211 lelttrd φBA<BAR
213 ltdivmul BARBA0<BABABA<RBA<BAR
214 151 66 64 128 213 syl112anc φBABA<RBA<BAR
215 212 214 mpbird φBABA<R
216 150 215 eqbrtrd φtanlogBA<R
217 55 136 66 138 216 lelttrd φlogBA<R
218 51 217 eqbrtrd φlogAlogB<R