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 = ℤRHom Z
rpvmasum.a φ N
rpvmasum.g G = DChr N
rpvmasum.d D = Base G
rpvmasum.1 1 ˙ = 0 G
Assertion rpvmasumlem φ x + n = 1 x 1 ˙ L n Λ n n log x 𝑂1

Proof

Step Hyp Ref Expression
1 rpvmasum.z Z = /N
2 rpvmasum.l L = ℤRHom Z
3 rpvmasum.a φ N
4 rpvmasum.g G = DChr N
5 rpvmasum.d D = Base G
6 rpvmasum.1 1 ˙ = 0 G
7 reex V
8 rpssre +
9 7 8 ssexi + V
10 9 a1i φ + V
11 fzfid φ 1 x Fin
12 elfznn n 1 x n
13 12 adantl φ n 1 x n
14 vmacl n Λ n
15 13 14 syl φ n 1 x Λ n
16 15 13 nndivred φ n 1 x Λ n n
17 16 recnd φ n 1 x Λ n n
18 11 17 fsumcl φ n = 1 x Λ n n
19 18 adantr φ x + n = 1 x Λ n n
20 relogcl x + log x
21 20 adantl φ x + log x
22 21 recnd φ x + log x
23 19 22 subcld φ x + n = 1 x Λ n n log x
24 1re 1
25 eqid Base Z = Base Z
26 4 1 6 25 3 dchr1re φ 1 ˙ : Base Z
27 26 adantr φ n 1 x 1 ˙ : Base Z
28 3 nnnn0d φ N 0
29 1 25 2 znzrhfo N 0 L : onto Base Z
30 fof L : onto Base Z L : Base Z
31 28 29 30 3syl φ L : Base Z
32 elfzelz n 1 x n
33 ffvelrn L : Base Z n L n Base Z
34 31 32 33 syl2an φ n 1 x L n Base Z
35 27 34 ffvelrnd φ n 1 x 1 ˙ L n
36 resubcl 1 1 ˙ L n 1 1 ˙ L n
37 24 35 36 sylancr φ n 1 x 1 1 ˙ L n
38 37 16 remulcld φ n 1 x 1 1 ˙ L n Λ n n
39 38 recnd φ n 1 x 1 1 ˙ L n Λ n n
40 11 39 fsumcl φ n = 1 x 1 1 ˙ L n Λ n n
41 40 adantr φ x + n = 1 x 1 1 ˙ L n Λ n n
42 eqidd φ x + n = 1 x Λ n n log x = x + n = 1 x Λ n n log x
43 eqidd φ x + n = 1 x 1 1 ˙ L n Λ n n = x + n = 1 x 1 1 ˙ L n Λ n n
44 10 23 41 42 43 offval2 φ x + n = 1 x Λ n n log x f x + n = 1 x 1 1 ˙ L n Λ n n = x + n = 1 x Λ n n - log x - n = 1 x 1 1 ˙ L n Λ n n
45 19 22 41 sub32d φ x + n = 1 x Λ n n - log x - n = 1 x 1 1 ˙ L n Λ n n = n = 1 x Λ n n - n = 1 x 1 1 ˙ L n Λ n n - log x
46 11 17 39 fsumsub φ n = 1 x Λ n n 1 1 ˙ L n Λ n n = n = 1 x Λ n n n = 1 x 1 1 ˙ L n Λ n n
47 1cnd φ n 1 x 1
48 37 recnd φ n 1 x 1 1 ˙ L n
49 47 48 17 subdird φ n 1 x 1 1 1 ˙ L n Λ n n = 1 Λ n n 1 1 ˙ L n Λ n n
50 ax-1cn 1
51 35 recnd φ n 1 x 1 ˙ L n
52 nncan 1 1 ˙ L n 1 1 1 ˙ L n = 1 ˙ L n
53 50 51 52 sylancr φ n 1 x 1 1 1 ˙ L n = 1 ˙ L n
54 53 oveq1d φ n 1 x 1 1 1 ˙ L n Λ n n = 1 ˙ L n Λ n n
55 17 mulid2d φ n 1 x 1 Λ n n = Λ n n
56 55 oveq1d φ n 1 x 1 Λ n n 1 1 ˙ L n Λ n n = Λ n n 1 1 ˙ L n Λ n n
57 49 54 56 3eqtr3rd φ n 1 x Λ n n 1 1 ˙ L n Λ n n = 1 ˙ L n Λ n n
58 57 sumeq2dv φ n = 1 x Λ n n 1 1 ˙ L n Λ n n = n = 1 x 1 ˙ L n Λ n n
59 46 58 eqtr3d φ n = 1 x Λ n n n = 1 x 1 1 ˙ L n Λ n n = n = 1 x 1 ˙ L n Λ n n
60 59 oveq1d φ n = 1 x Λ n n - n = 1 x 1 1 ˙ L n Λ n n - log x = n = 1 x 1 ˙ L n Λ n n log x
61 60 adantr φ x + n = 1 x Λ n n - n = 1 x 1 1 ˙ L n Λ n n - log x = n = 1 x 1 ˙ L n Λ n n log x
62 45 61 eqtrd φ x + n = 1 x Λ n n - log x - n = 1 x 1 1 ˙ L n Λ n n = n = 1 x 1 ˙ L n Λ n n log x
63 62 mpteq2dva φ x + n = 1 x Λ n n - log x - n = 1 x 1 1 ˙ L n Λ n n = x + n = 1 x 1 ˙ L n Λ n n log x
64 44 63 eqtrd φ x + n = 1 x Λ n n log x f x + n = 1 x 1 1 ˙ L n Λ n n = x + n = 1 x 1 ˙ L n Λ n n log x
65 vmadivsum x + n = 1 x Λ n n log x 𝑂1
66 8 a1i φ +
67 1red φ 1
68 prmdvdsfi N q | q N Fin
69 3 68 syl φ q | q N Fin
70 elrabi p q | q N p
71 prmnn p p
72 71 adantl φ p p
73 72 nnrpd φ p p +
74 73 relogcld φ p log p
75 prmuz2 p p 2
76 75 adantl φ p p 2
77 uz2m1nn p 2 p 1
78 76 77 syl φ p p 1
79 74 78 nndivred φ p log p p 1
80 70 79 sylan2 φ p q | q N log p p 1
81 69 80 fsumrecl φ p q | q N log p p 1
82 fzfid φ x + 1 x 1 x Fin
83 simpr φ x + 1 x n 1 x 1 ˙ L n = 0 1 ˙ L n = 0
84 0re 0
85 83 84 eqeltrdi φ x + 1 x n 1 x 1 ˙ L n = 0 1 ˙ L n
86 eqid Unit Z = Unit Z
87 3 ad3antrrr φ x + 1 x n 1 x 1 ˙ L n 0 N
88 4 dchrabl N G Abel
89 ablgrp G Abel G Grp
90 5 6 grpidcl G Grp 1 ˙ D
91 3 88 89 90 4syl φ 1 ˙ D
92 91 ad2antrr φ x + 1 x n 1 x 1 ˙ D
93 34 adantlr φ x + 1 x n 1 x L n Base Z
94 4 1 5 25 86 92 93 dchrn0 φ x + 1 x n 1 x 1 ˙ L n 0 L n Unit Z
95 94 biimpa φ x + 1 x n 1 x 1 ˙ L n 0 L n Unit Z
96 4 1 6 86 87 95 dchr1 φ x + 1 x n 1 x 1 ˙ L n 0 1 ˙ L n = 1
97 96 24 eqeltrdi φ x + 1 x n 1 x 1 ˙ L n 0 1 ˙ L n
98 85 97 pm2.61dane φ x + 1 x n 1 x 1 ˙ L n
99 24 98 36 sylancr φ x + 1 x n 1 x 1 1 ˙ L n
100 16 adantlr φ x + 1 x n 1 x Λ n n
101 99 100 remulcld φ x + 1 x n 1 x 1 1 ˙ L n Λ n n
102 82 101 fsumrecl φ x + 1 x n = 1 x 1 1 ˙ L n Λ n n
103 0le1 0 1
104 83 103 eqbrtrdi φ x + 1 x n 1 x 1 ˙ L n = 0 1 ˙ L n 1
105 24 leidi 1 1
106 96 105 eqbrtrdi φ x + 1 x n 1 x 1 ˙ L n 0 1 ˙ L n 1
107 104 106 pm2.61dane φ x + 1 x n 1 x 1 ˙ L n 1
108 subge0 1 1 ˙ L n 0 1 1 ˙ L n 1 ˙ L n 1
109 24 98 108 sylancr φ x + 1 x n 1 x 0 1 1 ˙ L n 1 ˙ L n 1
110 107 109 mpbird φ x + 1 x n 1 x 0 1 1 ˙ L n
111 15 adantlr φ x + 1 x n 1 x Λ n
112 12 adantl φ x + 1 x n 1 x n
113 vmage0 n 0 Λ n
114 112 113 syl φ x + 1 x n 1 x 0 Λ n
115 112 nnred φ x + 1 x n 1 x n
116 112 nngt0d φ x + 1 x n 1 x 0 < n
117 divge0 Λ n 0 Λ n n 0 < n 0 Λ n n
118 111 114 115 116 117 syl22anc φ x + 1 x n 1 x 0 Λ n n
119 99 100 110 118 mulge0d φ x + 1 x n 1 x 0 1 1 ˙ L n Λ n n
120 82 101 119 fsumge0 φ x + 1 x 0 n = 1 x 1 1 ˙ L n Λ n n
121 102 120 absidd φ x + 1 x n = 1 x 1 1 ˙ L n Λ n n = n = 1 x 1 1 ˙ L n Λ n n
122 69 adantr φ x + 1 x q | q N Fin
123 inss2 0 x
124 rabss2 0 x q 0 x | q N q | q N
125 123 124 mp1i φ x + 1 x q 0 x | q N q | q N
126 122 125 ssfid φ x + 1 x q 0 x | q N Fin
127 ssrab2 q 0 x | q N 0 x
128 127 123 sstri q 0 x | q N
129 128 sseli p q 0 x | q N p
130 79 adantlr φ x + 1 x p log p p 1
131 129 130 sylan2 φ x + 1 x p q 0 x | q N log p p 1
132 126 131 fsumrecl φ x + 1 x p q 0 x | q N log p p 1
133 81 adantr φ x + 1 x p q | q N log p p 1
134 2fveq3 n = p k 1 ˙ L n = 1 ˙ L p k
135 134 oveq2d n = p k 1 1 ˙ L n = 1 1 ˙ L p k
136 fveq2 n = p k Λ n = Λ p k
137 id n = p k n = p k
138 136 137 oveq12d n = p k Λ n n = Λ p k p k
139 135 138 oveq12d n = p k 1 1 ˙ L n Λ n n = 1 1 ˙ L p k Λ p k p k
140 rpre x + x
141 140 ad2antrl φ x + 1 x x
142 39 adantlr φ x + 1 x n 1 x 1 1 ˙ L n Λ n n
143 simprr φ x + 1 x n 1 x Λ n = 0 Λ n = 0
144 143 oveq1d φ x + 1 x n 1 x Λ n = 0 Λ n n = 0 n
145 12 ad2antrl φ x + 1 x n 1 x Λ n = 0 n
146 145 nncnd φ x + 1 x n 1 x Λ n = 0 n
147 145 nnne0d φ x + 1 x n 1 x Λ n = 0 n 0
148 146 147 div0d φ x + 1 x n 1 x Λ n = 0 0 n = 0
149 144 148 eqtrd φ x + 1 x n 1 x Λ n = 0 Λ n n = 0
150 149 oveq2d φ x + 1 x n 1 x Λ n = 0 1 1 ˙ L n Λ n n = 1 1 ˙ L n 0
151 48 ad2ant2r φ x + 1 x n 1 x Λ n = 0 1 1 ˙ L n
152 151 mul01d φ x + 1 x n 1 x Λ n = 0 1 1 ˙ L n 0 = 0
153 150 152 eqtrd φ x + 1 x n 1 x Λ n = 0 1 1 ˙ L n Λ n n = 0
154 139 141 142 153 fsumvma2 φ x + 1 x n = 1 x 1 1 ˙ L n Λ n n = p 0 x k = 1 log x log p 1 1 ˙ L p k Λ p k p k
155 127 a1i φ x + 1 x q 0 x | q N 0 x
156 fzfid φ x + 1 x p 1 log x log p Fin
157 26 ad2antrr φ x + 1 x p k 1 log x log p 1 ˙ : Base Z
158 31 ad2antrr φ x + 1 x p k 1 log x log p L : Base Z
159 71 ad2antrl φ x + 1 x p k 1 log x log p p
160 elfznn k 1 log x log p k
161 160 ad2antll φ x + 1 x p k 1 log x log p k
162 161 nnnn0d φ x + 1 x p k 1 log x log p k 0
163 159 162 nnexpcld φ x + 1 x p k 1 log x log p p k
164 163 nnzd φ x + 1 x p k 1 log x log p p k
165 158 164 ffvelrnd φ x + 1 x p k 1 log x log p L p k Base Z
166 157 165 ffvelrnd φ x + 1 x p k 1 log x log p 1 ˙ L p k
167 resubcl 1 1 ˙ L p k 1 1 ˙ L p k
168 24 166 167 sylancr φ x + 1 x p k 1 log x log p 1 1 ˙ L p k
169 vmacl p k Λ p k
170 163 169 syl φ x + 1 x p k 1 log x log p Λ p k
171 170 163 nndivred φ x + 1 x p k 1 log x log p Λ p k p k
172 168 171 remulcld φ x + 1 x p k 1 log x log p 1 1 ˙ L p k Λ p k p k
173 172 anassrs φ x + 1 x p k 1 log x log p 1 1 ˙ L p k Λ p k p k
174 173 recnd φ x + 1 x p k 1 log x log p 1 1 ˙ L p k Λ p k p k
175 156 174 fsumcl φ x + 1 x p k = 1 log x log p 1 1 ˙ L p k Λ p k p k
176 129 175 sylan2 φ x + 1 x p q 0 x | q N k = 1 log x log p 1 1 ˙ L p k Λ p k p k
177 breq1 q = p q N p N
178 177 notbid q = p ¬ q N ¬ p N
179 notrab 0 x q 0 x | q N = q 0 x | ¬ q N
180 178 179 elrab2 p 0 x q 0 x | q N p 0 x ¬ p N
181 123 sseli p 0 x p
182 3 ad3antrrr φ x + 1 x p ¬ p N k 1 log x log p N
183 simplrr φ x + 1 x p ¬ p N k 1 log x log p ¬ p N
184 simplrl φ x + 1 x p ¬ p N k 1 log x log p p
185 182 nnzd φ x + 1 x p ¬ p N k 1 log x log p N
186 coprm p N ¬ p N p gcd N = 1
187 184 185 186 syl2anc φ x + 1 x p ¬ p N k 1 log x log p ¬ p N p gcd N = 1
188 183 187 mpbid φ x + 1 x p ¬ p N k 1 log x log p p gcd N = 1
189 prmz p p
190 184 189 syl φ x + 1 x p ¬ p N k 1 log x log p p
191 160 adantl φ x + 1 x p ¬ p N k 1 log x log p k
192 191 nnnn0d φ x + 1 x p ¬ p N k 1 log x log p k 0
193 rpexp1i p N k 0 p gcd N = 1 p k gcd N = 1
194 190 185 192 193 syl3anc φ x + 1 x p ¬ p N k 1 log x log p p gcd N = 1 p k gcd N = 1
195 188 194 mpd φ x + 1 x p ¬ p N k 1 log x log p p k gcd N = 1
196 182 nnnn0d φ x + 1 x p ¬ p N k 1 log x log p N 0
197 164 anassrs φ x + 1 x p k 1 log x log p p k
198 197 adantlrr φ x + 1 x p ¬ p N k 1 log x log p p k
199 1 86 2 znunit N 0 p k L p k Unit Z p k gcd N = 1
200 196 198 199 syl2anc φ x + 1 x p ¬ p N k 1 log x log p L p k Unit Z p k gcd N = 1
201 195 200 mpbird φ x + 1 x p ¬ p N k 1 log x log p L p k Unit Z
202 4 1 6 86 182 201 dchr1 φ x + 1 x p ¬ p N k 1 log x log p 1 ˙ L p k = 1
203 202 oveq2d φ x + 1 x p ¬ p N k 1 log x log p 1 1 ˙ L p k = 1 1
204 1m1e0 1 1 = 0
205 203 204 eqtrdi φ x + 1 x p ¬ p N k 1 log x log p 1 1 ˙ L p k = 0
206 205 oveq1d φ x + 1 x p ¬ p N k 1 log x log p 1 1 ˙ L p k Λ p k p k = 0 Λ p k p k
207 171 recnd φ x + 1 x p k 1 log x log p Λ p k p k
208 207 anassrs φ x + 1 x p k 1 log x log p Λ p k p k
209 208 adantlrr φ x + 1 x p ¬ p N k 1 log x log p Λ p k p k
210 209 mul02d φ x + 1 x p ¬ p N k 1 log x log p 0 Λ p k p k = 0
211 206 210 eqtrd φ x + 1 x p ¬ p N k 1 log x log p 1 1 ˙ L p k Λ p k p k = 0
212 211 sumeq2dv φ x + 1 x p ¬ p N k = 1 log x log p 1 1 ˙ L p k Λ p k p k = k = 1 log x log p 0
213 fzfid φ x + 1 x p ¬ p N 1 log x log p Fin
214 213 olcd φ x + 1 x p ¬ p N 1 log x log p 1 1 log x log p Fin
215 sumz 1 log x log p 1 1 log x log p Fin k = 1 log x log p 0 = 0
216 214 215 syl φ x + 1 x p ¬ p N k = 1 log x log p 0 = 0
217 212 216 eqtrd φ x + 1 x p ¬ p N k = 1 log x log p 1 1 ˙ L p k Λ p k p k = 0
218 181 217 sylanr1 φ x + 1 x p 0 x ¬ p N k = 1 log x log p 1 1 ˙ L p k Λ p k p k = 0
219 180 218 sylan2b φ x + 1 x p 0 x q 0 x | q N k = 1 log x log p 1 1 ˙ L p k Λ p k p k = 0
220 ppifi x 0 x Fin
221 141 220 syl φ x + 1 x 0 x Fin
222 155 176 219 221 fsumss φ x + 1 x p q 0 x | q N k = 1 log x log p 1 1 ˙ L p k Λ p k p k = p 0 x k = 1 log x log p 1 1 ˙ L p k Λ p k p k
223 154 222 eqtr4d φ x + 1 x n = 1 x 1 1 ˙ L n Λ n n = p q 0 x | q N k = 1 log x log p 1 1 ˙ L p k Λ p k p k
224 156 173 fsumrecl φ x + 1 x p k = 1 log x log p 1 1 ˙ L p k Λ p k p k
225 129 224 sylan2 φ x + 1 x p q 0 x | q N k = 1 log x log p 1 1 ˙ L p k Λ p k p k
226 74 adantlr φ x + 1 x p log p
227 71 adantl φ x + 1 x p p
228 227 nnrecred φ x + 1 x p 1 p
229 227 nnrpd φ x + 1 x p p +
230 229 rpreccld φ x + 1 x p 1 p +
231 simplrl φ x + 1 x p x +
232 231 relogcld φ x + 1 x p log x
233 227 nnred φ x + 1 x p p
234 75 adantl φ x + 1 x p p 2
235 eluz2gt1 p 2 1 < p
236 234 235 syl φ x + 1 x p 1 < p
237 233 236 rplogcld φ x + 1 x p log p +
238 232 237 rerpdivcld φ x + 1 x p log x log p
239 238 flcld φ x + 1 x p log x log p
240 239 peano2zd φ x + 1 x p log x log p + 1
241 230 240 rpexpcld φ x + 1 x p 1 p log x log p + 1 +
242 241 rpred φ x + 1 x p 1 p log x log p + 1
243 228 242 resubcld φ x + 1 x p 1 p 1 p log x log p + 1
244 234 77 syl φ x + 1 x p p 1
245 244 nnrpd φ x + 1 x p p 1 +
246 245 229 rpdivcld φ x + 1 x p p 1 p +
247 243 246 rerpdivcld φ x + 1 x p 1 p 1 p log x log p + 1 p 1 p
248 226 247 remulcld φ x + 1 x p log p 1 p 1 p log x log p + 1 p 1 p
249 170 recnd φ x + 1 x p k 1 log x log p Λ p k
250 163 nncnd φ x + 1 x p k 1 log x log p p k
251 163 nnne0d φ x + 1 x p k 1 log x log p p k 0
252 249 250 251 divrecd φ x + 1 x p k 1 log x log p Λ p k p k = Λ p k 1 p k
253 simprl φ x + 1 x p k 1 log x log p p
254 vmappw p k Λ p k = log p
255 253 161 254 syl2anc φ x + 1 x p k 1 log x log p Λ p k = log p
256 159 nncnd φ x + 1 x p k 1 log x log p p
257 159 nnne0d φ x + 1 x p k 1 log x log p p 0
258 elfzelz k 1 log x log p k
259 258 ad2antll φ x + 1 x p k 1 log x log p k
260 256 257 259 exprecd φ x + 1 x p k 1 log x log p 1 p k = 1 p k
261 260 eqcomd φ x + 1 x p k 1 log x log p 1 p k = 1 p k
262 255 261 oveq12d φ x + 1 x p k 1 log x log p Λ p k 1 p k = log p 1 p k
263 252 262 eqtrd φ x + 1 x p k 1 log x log p Λ p k p k = log p 1 p k
264 263 171 eqeltrrd φ x + 1 x p k 1 log x log p log p 1 p k
265 264 anassrs φ x + 1 x p k 1 log x log p log p 1 p k
266 1red φ x + 1 x p k 1 log x log p 1
267 vmage0 p k 0 Λ p k
268 163 267 syl φ x + 1 x p k 1 log x log p 0 Λ p k
269 163 nnred φ x + 1 x p k 1 log x log p p k
270 163 nngt0d φ x + 1 x p k 1 log x log p 0 < p k
271 divge0 Λ p k 0 Λ p k p k 0 < p k 0 Λ p k p k
272 170 268 269 270 271 syl22anc φ x + 1 x p k 1 log x log p 0 Λ p k p k
273 84 leidi 0 0
274 simpr φ x + 1 x p k 1 log x log p 1 ˙ L p k = 0 1 ˙ L p k = 0
275 273 274 breqtrrid φ x + 1 x p k 1 log x log p 1 ˙ L p k = 0 0 1 ˙ L p k
276 3 ad3antrrr φ x + 1 x p k 1 log x log p 1 ˙ L p k 0 N
277 91 ad2antrr φ x + 1 x p k 1 log x log p 1 ˙ D
278 4 1 5 25 86 277 165 dchrn0 φ x + 1 x p k 1 log x log p 1 ˙ L p k 0 L p k Unit Z
279 278 biimpa φ x + 1 x p k 1 log x log p 1 ˙ L p k 0 L p k Unit Z
280 4 1 6 86 276 279 dchr1 φ x + 1 x p k 1 log x log p 1 ˙ L p k 0 1 ˙ L p k = 1
281 103 280 breqtrrid φ x + 1 x p k 1 log x log p 1 ˙ L p k 0 0 1 ˙ L p k
282 275 281 pm2.61dane φ x + 1 x p k 1 log x log p 0 1 ˙ L p k
283 subge02 1 1 ˙ L p k 0 1 ˙ L p k 1 1 ˙ L p k 1
284 24 166 283 sylancr φ x + 1 x p k 1 log x log p 0 1 ˙ L p k 1 1 ˙ L p k 1
285 282 284 mpbid φ x + 1 x p k 1 log x log p 1 1 ˙ L p k 1
286 168 266 171 272 285 lemul1ad φ x + 1 x p k 1 log x log p 1 1 ˙ L p k Λ p k p k 1 Λ p k p k
287 207 mulid2d φ x + 1 x p k 1 log x log p 1 Λ p k p k = Λ p k p k
288 287 263 eqtrd φ x + 1 x p k 1 log x log p 1 Λ p k p k = log p 1 p k
289 286 288 breqtrd φ x + 1 x p k 1 log x log p 1 1 ˙ L p k Λ p k p k log p 1 p k
290 289 anassrs φ x + 1 x p k 1 log x log p 1 1 ˙ L p k Λ p k p k log p 1 p k
291 156 173 265 290 fsumle φ x + 1 x p k = 1 log x log p 1 1 ˙ L p k Λ p k p k k = 1 log x log p log p 1 p k
292 226 recnd φ x + 1 x p log p
293 159 nnrecred φ x + 1 x p k 1 log x log p 1 p
294 293 162 reexpcld φ x + 1 x p k 1 log x log p 1 p k
295 294 recnd φ x + 1 x p k 1 log x log p 1 p k
296 295 anassrs φ x + 1 x p k 1 log x log p 1 p k
297 156 292 296 fsummulc2 φ x + 1 x p log p k = 1 log x log p 1 p k = k = 1 log x log p log p 1 p k
298 fzval3 log x log p 1 log x log p = 1 ..^ log x log p + 1
299 239 298 syl φ x + 1 x p 1 log x log p = 1 ..^ log x log p + 1
300 299 sumeq1d φ x + 1 x p k = 1 log x log p 1 p k = k 1 ..^ log x log p + 1 1 p k
301 228 recnd φ x + 1 x p 1 p
302 227 nngt0d φ x + 1 x p 0 < p
303 recgt1 p 0 < p 1 < p 1 p < 1
304 233 302 303 syl2anc φ x + 1 x p 1 < p 1 p < 1
305 236 304 mpbid φ x + 1 x p 1 p < 1
306 228 305 ltned φ x + 1 x p 1 p 1
307 1nn0 1 0
308 307 a1i φ x + 1 x p 1 0
309 log1 log 1 = 0
310 simprr φ x + 1 x 1 x
311 1rp 1 +
312 simprl φ x + 1 x x +
313 logleb 1 + x + 1 x log 1 log x
314 311 312 313 sylancr φ x + 1 x 1 x log 1 log x
315 310 314 mpbid φ x + 1 x log 1 log x
316 309 315 eqbrtrrid φ x + 1 x 0 log x
317 316 adantr φ x + 1 x p 0 log x
318 232 237 317 divge0d φ x + 1 x p 0 log x log p
319 flge0nn0 log x log p 0 log x log p log x log p 0
320 238 318 319 syl2anc φ x + 1 x p log x log p 0
321 nn0p1nn log x log p 0 log x log p + 1
322 320 321 syl φ x + 1 x p log x log p + 1
323 nnuz = 1
324 322 323 eleqtrdi φ x + 1 x p log x log p + 1 1
325 301 306 308 324 geoserg φ x + 1 x p k 1 ..^ log x log p + 1 1 p k = 1 p 1 1 p log x log p + 1 1 1 p
326 301 exp1d φ x + 1 x p 1 p 1 = 1 p
327 326 oveq1d φ x + 1 x p 1 p 1 1 p log x log p + 1 = 1 p 1 p log x log p + 1
328 227 nncnd φ x + 1 x p p
329 1cnd φ x + 1 x p 1
330 229 rpcnne0d φ x + 1 x p p p 0
331 divsubdir p 1 p p 0 p 1 p = p p 1 p
332 328 329 330 331 syl3anc φ x + 1 x p p 1 p = p p 1 p
333 divid p p 0 p p = 1
334 330 333 syl φ x + 1 x p p p = 1
335 334 oveq1d φ x + 1 x p p p 1 p = 1 1 p
336 332 335 eqtr2d φ x + 1 x p 1 1 p = p 1 p
337 327 336 oveq12d φ x + 1 x p 1 p 1 1 p log x log p + 1 1 1 p = 1 p 1 p log x log p + 1 p 1 p
338 300 325 337 3eqtrd φ x + 1 x p k = 1 log x log p 1 p k = 1 p 1 p log x log p + 1 p 1 p
339 338 oveq2d φ x + 1 x p log p k = 1 log x log p 1 p k = log p 1 p 1 p log x log p + 1 p 1 p
340 297 339 eqtr3d φ x + 1 x p k = 1 log x log p log p 1 p k = log p 1 p 1 p log x log p + 1 p 1 p
341 291 340 breqtrd φ x + 1 x p k = 1 log x log p 1 1 ˙ L p k Λ p k p k log p 1 p 1 p log x log p + 1 p 1 p
342 241 rpge0d φ x + 1 x p 0 1 p log x log p + 1
343 228 242 subge02d φ x + 1 x p 0 1 p log x log p + 1 1 p 1 p log x log p + 1 1 p
344 342 343 mpbid φ x + 1 x p 1 p 1 p log x log p + 1 1 p
345 245 rpcnne0d φ x + 1 x p p 1 p 1 0
346 dmdcan p 1 p 1 0 p p 0 1 p 1 p 1 p 1 = 1 p
347 345 330 329 346 syl3anc φ x + 1 x p p 1 p 1 p 1 = 1 p
348 344 347 breqtrrd φ x + 1 x p 1 p 1 p log x log p + 1 p 1 p 1 p 1
349 244 nnrecred φ x + 1 x p 1 p 1
350 243 349 246 ledivmuld φ x + 1 x p 1 p 1 p log x log p + 1 p 1 p 1 p 1 1 p 1 p log x log p + 1 p 1 p 1 p 1
351 348 350 mpbird φ x + 1 x p 1 p 1 p log x log p + 1 p 1 p 1 p 1
352 247 349 237 lemul2d φ x + 1 x p 1 p 1 p log x log p + 1 p 1 p 1 p 1 log p 1 p 1 p log x log p + 1 p 1 p log p 1 p 1
353 351 352 mpbid φ x + 1 x p log p 1 p 1 p log x log p + 1 p 1 p log p 1 p 1
354 244 nncnd φ x + 1 x p p 1
355 244 nnne0d φ x + 1 x p p 1 0
356 292 354 355 divrecd φ x + 1 x p log p p 1 = log p 1 p 1
357 353 356 breqtrrd φ x + 1 x p log p 1 p 1 p log x log p + 1 p 1 p log p p 1
358 224 248 130 341 357 letrd φ x + 1 x p k = 1 log x log p 1 1 ˙ L p k Λ p k p k log p p 1
359 129 358 sylan2 φ x + 1 x p q 0 x | q N k = 1 log x log p 1 1 ˙ L p k Λ p k p k log p p 1
360 126 225 131 359 fsumle φ x + 1 x p q 0 x | q N k = 1 log x log p 1 1 ˙ L p k Λ p k p k p q 0 x | q N log p p 1
361 223 360 eqbrtrd φ x + 1 x n = 1 x 1 1 ˙ L n Λ n n p q 0 x | q N log p p 1
362 80 adantlr φ x + 1 x p q | q N log p p 1
363 237 245 rpdivcld φ x + 1 x p log p p 1 +
364 363 rpge0d φ x + 1 x p 0 log p p 1
365 70 364 sylan2 φ x + 1 x p q | q N 0 log p p 1
366 122 362 365 125 fsumless φ x + 1 x p q 0 x | q N log p p 1 p q | q N log p p 1
367 102 132 133 361 366 letrd φ x + 1 x n = 1 x 1 1 ˙ L n Λ n n p q | q N log p p 1
368 121 367 eqbrtrd φ x + 1 x n = 1 x 1 1 ˙ L n Λ n n p q | q N log p p 1
369 66 41 67 81 368 elo1d φ x + n = 1 x 1 1 ˙ L n Λ n n 𝑂1
370 o1sub x + n = 1 x Λ n n log x 𝑂1 x + n = 1 x 1 1 ˙ L n Λ n n 𝑂1 x + n = 1 x Λ n n log x f x + n = 1 x 1 1 ˙ L n Λ n n 𝑂1
371 65 369 370 sylancr φ x + n = 1 x Λ n n log x f x + n = 1 x 1 1 ˙ L n Λ n n 𝑂1
372 64 371 eqeltrrd φ x + n = 1 x 1 ˙ L n Λ n n log x 𝑂1