Metamath Proof Explorer


Theorem rpvmasumlem

Description: Lemma for rpvmasum . Calculate the "trivial case" estimate sum_ n <_ x ( .1. ( n ) Lam ( n ) / n ) = log x + O(1) , where .1. ( x ) is the principal Dirichlet character. Equation 9.4.7 of Shapiro, p. 376. (Contributed by Mario Carneiro, 2-May-2016)

Ref Expression
Hypotheses rpvmasum.z Z=/N
rpvmasum.l L=ℤRHomZ
rpvmasum.a φN
rpvmasum.g G=DChrN
rpvmasum.d D=BaseG
rpvmasum.1 1˙=0G
Assertion rpvmasumlem φx+n=1x1˙LnΛnnlogx𝑂1

Proof

Step Hyp Ref Expression
1 rpvmasum.z Z=/N
2 rpvmasum.l L=ℤRHomZ
3 rpvmasum.a φN
4 rpvmasum.g G=DChrN
5 rpvmasum.d D=BaseG
6 rpvmasum.1 1˙=0G
7 reex V
8 rpssre +
9 7 8 ssexi +V
10 9 a1i φ+V
11 fzfid φ1xFin
12 elfznn n1xn
13 12 adantl φn1xn
14 vmacl nΛn
15 13 14 syl φn1xΛn
16 15 13 nndivred φn1xΛnn
17 16 recnd φn1xΛnn
18 11 17 fsumcl φn=1xΛnn
19 18 adantr φx+n=1xΛnn
20 relogcl x+logx
21 20 adantl φx+logx
22 21 recnd φx+logx
23 19 22 subcld φx+n=1xΛnnlogx
24 1re 1
25 eqid BaseZ=BaseZ
26 4 1 6 25 3 dchr1re φ1˙:BaseZ
27 26 adantr φn1x1˙:BaseZ
28 3 nnnn0d φN0
29 1 25 2 znzrhfo N0L:ontoBaseZ
30 fof L:ontoBaseZL:BaseZ
31 28 29 30 3syl φL:BaseZ
32 elfzelz n1xn
33 ffvelrn L:BaseZnLnBaseZ
34 31 32 33 syl2an φn1xLnBaseZ
35 27 34 ffvelrnd φn1x1˙Ln
36 resubcl 11˙Ln11˙Ln
37 24 35 36 sylancr φn1x11˙Ln
38 37 16 remulcld φn1x11˙LnΛnn
39 38 recnd φn1x11˙LnΛnn
40 11 39 fsumcl φn=1x11˙LnΛnn
41 40 adantr φx+n=1x11˙LnΛnn
42 eqidd φx+n=1xΛnnlogx=x+n=1xΛnnlogx
43 eqidd φx+n=1x11˙LnΛnn=x+n=1x11˙LnΛnn
44 10 23 41 42 43 offval2 φx+n=1xΛnnlogxfx+n=1x11˙LnΛnn=x+n=1xΛnn-logx-n=1x11˙LnΛnn
45 19 22 41 sub32d φx+n=1xΛnn-logx-n=1x11˙LnΛnn=n=1xΛnn-n=1x11˙LnΛnn-logx
46 11 17 39 fsumsub φn=1xΛnn11˙LnΛnn=n=1xΛnnn=1x11˙LnΛnn
47 1cnd φn1x1
48 37 recnd φn1x11˙Ln
49 47 48 17 subdird φn1x111˙LnΛnn=1Λnn11˙LnΛnn
50 ax-1cn 1
51 35 recnd φn1x1˙Ln
52 nncan 11˙Ln111˙Ln=1˙Ln
53 50 51 52 sylancr φn1x111˙Ln=1˙Ln
54 53 oveq1d φn1x111˙LnΛnn=1˙LnΛnn
55 17 mulid2d φn1x1Λnn=Λnn
56 55 oveq1d φn1x1Λnn11˙LnΛnn=Λnn11˙LnΛnn
57 49 54 56 3eqtr3rd φn1xΛnn11˙LnΛnn=1˙LnΛnn
58 57 sumeq2dv φn=1xΛnn11˙LnΛnn=n=1x1˙LnΛnn
59 46 58 eqtr3d φn=1xΛnnn=1x11˙LnΛnn=n=1x1˙LnΛnn
60 59 oveq1d φn=1xΛnn-n=1x11˙LnΛnn-logx=n=1x1˙LnΛnnlogx
61 60 adantr φx+n=1xΛnn-n=1x11˙LnΛnn-logx=n=1x1˙LnΛnnlogx
62 45 61 eqtrd φx+n=1xΛnn-logx-n=1x11˙LnΛnn=n=1x1˙LnΛnnlogx
63 62 mpteq2dva φx+n=1xΛnn-logx-n=1x11˙LnΛnn=x+n=1x1˙LnΛnnlogx
64 44 63 eqtrd φx+n=1xΛnnlogxfx+n=1x11˙LnΛnn=x+n=1x1˙LnΛnnlogx
65 vmadivsum x+n=1xΛnnlogx𝑂1
66 8 a1i φ+
67 1red φ1
68 prmdvdsfi Nq|qNFin
69 3 68 syl φq|qNFin
70 elrabi pq|qNp
71 prmnn pp
72 71 adantl φpp
73 72 nnrpd φpp+
74 73 relogcld φplogp
75 prmuz2 pp2
76 75 adantl φpp2
77 uz2m1nn p2p1
78 76 77 syl φpp1
79 74 78 nndivred φplogpp1
80 70 79 sylan2 φpq|qNlogpp1
81 69 80 fsumrecl φpq|qNlogpp1
82 fzfid φx+1x1xFin
83 simpr φx+1xn1x1˙Ln=01˙Ln=0
84 0re 0
85 83 84 eqeltrdi φx+1xn1x1˙Ln=01˙Ln
86 eqid UnitZ=UnitZ
87 3 ad3antrrr φx+1xn1x1˙Ln0N
88 4 dchrabl NGAbel
89 ablgrp GAbelGGrp
90 5 6 grpidcl GGrp1˙D
91 3 88 89 90 4syl φ1˙D
92 91 ad2antrr φx+1xn1x1˙D
93 34 adantlr φx+1xn1xLnBaseZ
94 4 1 5 25 86 92 93 dchrn0 φx+1xn1x1˙Ln0LnUnitZ
95 94 biimpa φx+1xn1x1˙Ln0LnUnitZ
96 4 1 6 86 87 95 dchr1 φx+1xn1x1˙Ln01˙Ln=1
97 96 24 eqeltrdi φx+1xn1x1˙Ln01˙Ln
98 85 97 pm2.61dane φx+1xn1x1˙Ln
99 24 98 36 sylancr φx+1xn1x11˙Ln
100 16 adantlr φx+1xn1xΛnn
101 99 100 remulcld φx+1xn1x11˙LnΛnn
102 82 101 fsumrecl φx+1xn=1x11˙LnΛnn
103 0le1 01
104 83 103 eqbrtrdi φx+1xn1x1˙Ln=01˙Ln1
105 24 leidi 11
106 96 105 eqbrtrdi φx+1xn1x1˙Ln01˙Ln1
107 104 106 pm2.61dane φx+1xn1x1˙Ln1
108 subge0 11˙Ln011˙Ln1˙Ln1
109 24 98 108 sylancr φx+1xn1x011˙Ln1˙Ln1
110 107 109 mpbird φx+1xn1x011˙Ln
111 15 adantlr φx+1xn1xΛn
112 12 adantl φx+1xn1xn
113 vmage0 n0Λn
114 112 113 syl φx+1xn1x0Λn
115 112 nnred φx+1xn1xn
116 112 nngt0d φx+1xn1x0<n
117 divge0 Λn0Λnn0<n0Λnn
118 111 114 115 116 117 syl22anc φx+1xn1x0Λnn
119 99 100 110 118 mulge0d φx+1xn1x011˙LnΛnn
120 82 101 119 fsumge0 φx+1x0n=1x11˙LnΛnn
121 102 120 absidd φx+1xn=1x11˙LnΛnn=n=1x11˙LnΛnn
122 69 adantr φx+1xq|qNFin
123 inss2 0x
124 rabss2 0xq0x|qNq|qN
125 123 124 mp1i φx+1xq0x|qNq|qN
126 122 125 ssfid φx+1xq0x|qNFin
127 ssrab2 q0x|qN0x
128 127 123 sstri q0x|qN
129 128 sseli pq0x|qNp
130 79 adantlr φx+1xplogpp1
131 129 130 sylan2 φx+1xpq0x|qNlogpp1
132 126 131 fsumrecl φx+1xpq0x|qNlogpp1
133 81 adantr φx+1xpq|qNlogpp1
134 2fveq3 n=pk1˙Ln=1˙Lpk
135 134 oveq2d n=pk11˙Ln=11˙Lpk
136 fveq2 n=pkΛn=Λpk
137 id n=pkn=pk
138 136 137 oveq12d n=pkΛnn=Λpkpk
139 135 138 oveq12d n=pk11˙LnΛnn=11˙LpkΛpkpk
140 rpre x+x
141 140 ad2antrl φx+1xx
142 39 adantlr φx+1xn1x11˙LnΛnn
143 simprr φx+1xn1xΛn=0Λn=0
144 143 oveq1d φx+1xn1xΛn=0Λnn=0n
145 12 ad2antrl φx+1xn1xΛn=0n
146 145 nncnd φx+1xn1xΛn=0n
147 145 nnne0d φx+1xn1xΛn=0n0
148 146 147 div0d φx+1xn1xΛn=00n=0
149 144 148 eqtrd φx+1xn1xΛn=0Λnn=0
150 149 oveq2d φx+1xn1xΛn=011˙LnΛnn=11˙Ln0
151 48 ad2ant2r φx+1xn1xΛn=011˙Ln
152 151 mul01d φx+1xn1xΛn=011˙Ln0=0
153 150 152 eqtrd φx+1xn1xΛn=011˙LnΛnn=0
154 139 141 142 153 fsumvma2 φx+1xn=1x11˙LnΛnn=p0xk=1logxlogp11˙LpkΛpkpk
155 127 a1i φx+1xq0x|qN0x
156 fzfid φx+1xp1logxlogpFin
157 26 ad2antrr φx+1xpk1logxlogp1˙:BaseZ
158 31 ad2antrr φx+1xpk1logxlogpL:BaseZ
159 71 ad2antrl φx+1xpk1logxlogpp
160 elfznn k1logxlogpk
161 160 ad2antll φx+1xpk1logxlogpk
162 161 nnnn0d φx+1xpk1logxlogpk0
163 159 162 nnexpcld φx+1xpk1logxlogppk
164 163 nnzd φx+1xpk1logxlogppk
165 158 164 ffvelrnd φx+1xpk1logxlogpLpkBaseZ
166 157 165 ffvelrnd φx+1xpk1logxlogp1˙Lpk
167 resubcl 11˙Lpk11˙Lpk
168 24 166 167 sylancr φx+1xpk1logxlogp11˙Lpk
169 vmacl pkΛpk
170 163 169 syl φx+1xpk1logxlogpΛpk
171 170 163 nndivred φx+1xpk1logxlogpΛpkpk
172 168 171 remulcld φx+1xpk1logxlogp11˙LpkΛpkpk
173 172 anassrs φx+1xpk1logxlogp11˙LpkΛpkpk
174 173 recnd φx+1xpk1logxlogp11˙LpkΛpkpk
175 156 174 fsumcl φx+1xpk=1logxlogp11˙LpkΛpkpk
176 129 175 sylan2 φx+1xpq0x|qNk=1logxlogp11˙LpkΛpkpk
177 breq1 q=pqNpN
178 177 notbid q=p¬qN¬pN
179 notrab 0xq0x|qN=q0x|¬qN
180 178 179 elrab2 p0xq0x|qNp0x¬pN
181 123 sseli p0xp
182 3 ad3antrrr φx+1xp¬pNk1logxlogpN
183 simplrr φx+1xp¬pNk1logxlogp¬pN
184 simplrl φx+1xp¬pNk1logxlogpp
185 182 nnzd φx+1xp¬pNk1logxlogpN
186 coprm pN¬pNpgcdN=1
187 184 185 186 syl2anc φx+1xp¬pNk1logxlogp¬pNpgcdN=1
188 183 187 mpbid φx+1xp¬pNk1logxlogppgcdN=1
189 prmz pp
190 184 189 syl φx+1xp¬pNk1logxlogpp
191 160 adantl φx+1xp¬pNk1logxlogpk
192 191 nnnn0d φx+1xp¬pNk1logxlogpk0
193 rpexp1i pNk0pgcdN=1pkgcdN=1
194 190 185 192 193 syl3anc φx+1xp¬pNk1logxlogppgcdN=1pkgcdN=1
195 188 194 mpd φx+1xp¬pNk1logxlogppkgcdN=1
196 182 nnnn0d φx+1xp¬pNk1logxlogpN0
197 164 anassrs φx+1xpk1logxlogppk
198 197 adantlrr φx+1xp¬pNk1logxlogppk
199 1 86 2 znunit N0pkLpkUnitZpkgcdN=1
200 196 198 199 syl2anc φx+1xp¬pNk1logxlogpLpkUnitZpkgcdN=1
201 195 200 mpbird φx+1xp¬pNk1logxlogpLpkUnitZ
202 4 1 6 86 182 201 dchr1 φx+1xp¬pNk1logxlogp1˙Lpk=1
203 202 oveq2d φx+1xp¬pNk1logxlogp11˙Lpk=11
204 1m1e0 11=0
205 203 204 eqtrdi φx+1xp¬pNk1logxlogp11˙Lpk=0
206 205 oveq1d φx+1xp¬pNk1logxlogp11˙LpkΛpkpk=0Λpkpk
207 171 recnd φx+1xpk1logxlogpΛpkpk
208 207 anassrs φx+1xpk1logxlogpΛpkpk
209 208 adantlrr φx+1xp¬pNk1logxlogpΛpkpk
210 209 mul02d φx+1xp¬pNk1logxlogp0Λpkpk=0
211 206 210 eqtrd φx+1xp¬pNk1logxlogp11˙LpkΛpkpk=0
212 211 sumeq2dv φx+1xp¬pNk=1logxlogp11˙LpkΛpkpk=k=1logxlogp0
213 fzfid φx+1xp¬pN1logxlogpFin
214 213 olcd φx+1xp¬pN1logxlogp11logxlogpFin
215 sumz 1logxlogp11logxlogpFink=1logxlogp0=0
216 214 215 syl φx+1xp¬pNk=1logxlogp0=0
217 212 216 eqtrd φx+1xp¬pNk=1logxlogp11˙LpkΛpkpk=0
218 181 217 sylanr1 φx+1xp0x¬pNk=1logxlogp11˙LpkΛpkpk=0
219 180 218 sylan2b φx+1xp0xq0x|qNk=1logxlogp11˙LpkΛpkpk=0
220 ppifi x0xFin
221 141 220 syl φx+1x0xFin
222 155 176 219 221 fsumss φx+1xpq0x|qNk=1logxlogp11˙LpkΛpkpk=p0xk=1logxlogp11˙LpkΛpkpk
223 154 222 eqtr4d φx+1xn=1x11˙LnΛnn=pq0x|qNk=1logxlogp11˙LpkΛpkpk
224 156 173 fsumrecl φx+1xpk=1logxlogp11˙LpkΛpkpk
225 129 224 sylan2 φx+1xpq0x|qNk=1logxlogp11˙LpkΛpkpk
226 74 adantlr φx+1xplogp
227 71 adantl φx+1xpp
228 227 nnrecred φx+1xp1p
229 227 nnrpd φx+1xpp+
230 229 rpreccld φx+1xp1p+
231 simplrl φx+1xpx+
232 231 relogcld φx+1xplogx
233 227 nnred φx+1xpp
234 75 adantl φx+1xpp2
235 eluz2gt1 p21<p
236 234 235 syl φx+1xp1<p
237 233 236 rplogcld φx+1xplogp+
238 232 237 rerpdivcld φx+1xplogxlogp
239 238 flcld φx+1xplogxlogp
240 239 peano2zd φx+1xplogxlogp+1
241 230 240 rpexpcld φx+1xp1plogxlogp+1+
242 241 rpred φx+1xp1plogxlogp+1
243 228 242 resubcld φx+1xp1p1plogxlogp+1
244 234 77 syl φx+1xpp1
245 244 nnrpd φx+1xpp1+
246 245 229 rpdivcld φx+1xpp1p+
247 243 246 rerpdivcld φx+1xp1p1plogxlogp+1p1p
248 226 247 remulcld φx+1xplogp1p1plogxlogp+1p1p
249 170 recnd φx+1xpk1logxlogpΛpk
250 163 nncnd φx+1xpk1logxlogppk
251 163 nnne0d φx+1xpk1logxlogppk0
252 249 250 251 divrecd φx+1xpk1logxlogpΛpkpk=Λpk1pk
253 simprl φx+1xpk1logxlogpp
254 vmappw pkΛpk=logp
255 253 161 254 syl2anc φx+1xpk1logxlogpΛpk=logp
256 159 nncnd φx+1xpk1logxlogpp
257 159 nnne0d φx+1xpk1logxlogpp0
258 elfzelz k1logxlogpk
259 258 ad2antll φx+1xpk1logxlogpk
260 256 257 259 exprecd φx+1xpk1logxlogp1pk=1pk
261 260 eqcomd φx+1xpk1logxlogp1pk=1pk
262 255 261 oveq12d φx+1xpk1logxlogpΛpk1pk=logp1pk
263 252 262 eqtrd φx+1xpk1logxlogpΛpkpk=logp1pk
264 263 171 eqeltrrd φx+1xpk1logxlogplogp1pk
265 264 anassrs φx+1xpk1logxlogplogp1pk
266 1red φx+1xpk1logxlogp1
267 vmage0 pk0Λpk
268 163 267 syl φx+1xpk1logxlogp0Λpk
269 163 nnred φx+1xpk1logxlogppk
270 163 nngt0d φx+1xpk1logxlogp0<pk
271 divge0 Λpk0Λpkpk0<pk0Λpkpk
272 170 268 269 270 271 syl22anc φx+1xpk1logxlogp0Λpkpk
273 84 leidi 00
274 simpr φx+1xpk1logxlogp1˙Lpk=01˙Lpk=0
275 273 274 breqtrrid φx+1xpk1logxlogp1˙Lpk=001˙Lpk
276 3 ad3antrrr φx+1xpk1logxlogp1˙Lpk0N
277 91 ad2antrr φx+1xpk1logxlogp1˙D
278 4 1 5 25 86 277 165 dchrn0 φx+1xpk1logxlogp1˙Lpk0LpkUnitZ
279 278 biimpa φx+1xpk1logxlogp1˙Lpk0LpkUnitZ
280 4 1 6 86 276 279 dchr1 φx+1xpk1logxlogp1˙Lpk01˙Lpk=1
281 103 280 breqtrrid φx+1xpk1logxlogp1˙Lpk001˙Lpk
282 275 281 pm2.61dane φx+1xpk1logxlogp01˙Lpk
283 subge02 11˙Lpk01˙Lpk11˙Lpk1
284 24 166 283 sylancr φx+1xpk1logxlogp01˙Lpk11˙Lpk1
285 282 284 mpbid φx+1xpk1logxlogp11˙Lpk1
286 168 266 171 272 285 lemul1ad φx+1xpk1logxlogp11˙LpkΛpkpk1Λpkpk
287 207 mulid2d φx+1xpk1logxlogp1Λpkpk=Λpkpk
288 287 263 eqtrd φx+1xpk1logxlogp1Λpkpk=logp1pk
289 286 288 breqtrd φx+1xpk1logxlogp11˙LpkΛpkpklogp1pk
290 289 anassrs φx+1xpk1logxlogp11˙LpkΛpkpklogp1pk
291 156 173 265 290 fsumle φx+1xpk=1logxlogp11˙LpkΛpkpkk=1logxlogplogp1pk
292 226 recnd φx+1xplogp
293 159 nnrecred φx+1xpk1logxlogp1p
294 293 162 reexpcld φx+1xpk1logxlogp1pk
295 294 recnd φx+1xpk1logxlogp1pk
296 295 anassrs φx+1xpk1logxlogp1pk
297 156 292 296 fsummulc2 φx+1xplogpk=1logxlogp1pk=k=1logxlogplogp1pk
298 fzval3 logxlogp1logxlogp=1..^logxlogp+1
299 239 298 syl φx+1xp1logxlogp=1..^logxlogp+1
300 299 sumeq1d φx+1xpk=1logxlogp1pk=k1..^logxlogp+11pk
301 228 recnd φx+1xp1p
302 227 nngt0d φx+1xp0<p
303 recgt1 p0<p1<p1p<1
304 233 302 303 syl2anc φx+1xp1<p1p<1
305 236 304 mpbid φx+1xp1p<1
306 228 305 ltned φx+1xp1p1
307 1nn0 10
308 307 a1i φx+1xp10
309 log1 log1=0
310 simprr φx+1x1x
311 1rp 1+
312 simprl φx+1xx+
313 logleb 1+x+1xlog1logx
314 311 312 313 sylancr φx+1x1xlog1logx
315 310 314 mpbid φx+1xlog1logx
316 309 315 eqbrtrrid φx+1x0logx
317 316 adantr φx+1xp0logx
318 232 237 317 divge0d φx+1xp0logxlogp
319 flge0nn0 logxlogp0logxlogplogxlogp0
320 238 318 319 syl2anc φx+1xplogxlogp0
321 nn0p1nn logxlogp0logxlogp+1
322 320 321 syl φx+1xplogxlogp+1
323 nnuz =1
324 322 323 eleqtrdi φx+1xplogxlogp+11
325 301 306 308 324 geoserg φx+1xpk1..^logxlogp+11pk=1p11plogxlogp+111p
326 301 exp1d φx+1xp1p1=1p
327 326 oveq1d φx+1xp1p11plogxlogp+1=1p1plogxlogp+1
328 227 nncnd φx+1xpp
329 1cnd φx+1xp1
330 229 rpcnne0d φx+1xppp0
331 divsubdir p1pp0p1p=pp1p
332 328 329 330 331 syl3anc φx+1xpp1p=pp1p
333 divid pp0pp=1
334 330 333 syl φx+1xppp=1
335 334 oveq1d φx+1xppp1p=11p
336 332 335 eqtr2d φx+1xp11p=p1p
337 327 336 oveq12d φx+1xp1p11plogxlogp+111p=1p1plogxlogp+1p1p
338 300 325 337 3eqtrd φx+1xpk=1logxlogp1pk=1p1plogxlogp+1p1p
339 338 oveq2d φx+1xplogpk=1logxlogp1pk=logp1p1plogxlogp+1p1p
340 297 339 eqtr3d φx+1xpk=1logxlogplogp1pk=logp1p1plogxlogp+1p1p
341 291 340 breqtrd φx+1xpk=1logxlogp11˙LpkΛpkpklogp1p1plogxlogp+1p1p
342 241 rpge0d φx+1xp01plogxlogp+1
343 228 242 subge02d φx+1xp01plogxlogp+11p1plogxlogp+11p
344 342 343 mpbid φx+1xp1p1plogxlogp+11p
345 245 rpcnne0d φx+1xpp1p10
346 dmdcan p1p10pp01p1p1p1=1p
347 345 330 329 346 syl3anc φx+1xpp1p1p1=1p
348 344 347 breqtrrd φx+1xp1p1plogxlogp+1p1p1p1
349 244 nnrecred φx+1xp1p1
350 243 349 246 ledivmuld φx+1xp1p1plogxlogp+1p1p1p11p1plogxlogp+1p1p1p1
351 348 350 mpbird φx+1xp1p1plogxlogp+1p1p1p1
352 247 349 237 lemul2d φx+1xp1p1plogxlogp+1p1p1p1logp1p1plogxlogp+1p1plogp1p1
353 351 352 mpbid φx+1xplogp1p1plogxlogp+1p1plogp1p1
354 244 nncnd φx+1xpp1
355 244 nnne0d φx+1xpp10
356 292 354 355 divrecd φx+1xplogpp1=logp1p1
357 353 356 breqtrrd φx+1xplogp1p1plogxlogp+1p1plogpp1
358 224 248 130 341 357 letrd φx+1xpk=1logxlogp11˙LpkΛpkpklogpp1
359 129 358 sylan2 φx+1xpq0x|qNk=1logxlogp11˙LpkΛpkpklogpp1
360 126 225 131 359 fsumle φx+1xpq0x|qNk=1logxlogp11˙LpkΛpkpkpq0x|qNlogpp1
361 223 360 eqbrtrd φx+1xn=1x11˙LnΛnnpq0x|qNlogpp1
362 80 adantlr φx+1xpq|qNlogpp1
363 237 245 rpdivcld φx+1xplogpp1+
364 363 rpge0d φx+1xp0logpp1
365 70 364 sylan2 φx+1xpq|qN0logpp1
366 122 362 365 125 fsumless φx+1xpq0x|qNlogpp1pq|qNlogpp1
367 102 132 133 361 366 letrd φx+1xn=1x11˙LnΛnnpq|qNlogpp1
368 121 367 eqbrtrd φx+1xn=1x11˙LnΛnnpq|qNlogpp1
369 66 41 67 81 368 elo1d φx+n=1x11˙LnΛnn𝑂1
370 o1sub x+n=1xΛnnlogx𝑂1x+n=1x11˙LnΛnn𝑂1x+n=1xΛnnlogxfx+n=1x11˙LnΛnn𝑂1
371 65 369 370 sylancr φx+n=1xΛnnlogxfx+n=1x11˙LnΛnn𝑂1
372 64 371 eqeltrrd φx+n=1x1˙LnΛnnlogx𝑂1