Metamath Proof Explorer


Theorem selberg2lem

Description: Lemma for selberg2 . Equation 10.4.12 of Shapiro, p. 420. (Contributed by Mario Carneiro, 23-May-2016)

Ref Expression
Assertion selberg2lem x + n = 1 x Λ n log n ψ x log x x 𝑂1

Proof

Step Hyp Ref Expression
1 rpre x + x
2 chpcl x ψ x
3 1 2 syl x + ψ x
4 3 recnd x + ψ x
5 rprege0 x + x 0 x
6 flge0nn0 x 0 x x 0
7 5 6 syl x + x 0
8 nn0p1nn x 0 x + 1
9 7 8 syl x + x + 1
10 9 nnrpd x + x + 1 +
11 10 relogcld x + log x + 1
12 11 recnd x + log x + 1
13 relogcl x + log x
14 13 recnd x + log x
15 12 14 subcld x + log x + 1 log x
16 4 15 mulcld x + ψ x log x + 1 log x
17 fzfid x + 1 x Fin
18 elfznn n 1 x n
19 18 adantl x + n 1 x n
20 19 nnrpd x + n 1 x n +
21 1rp 1 +
22 rpaddcl n + 1 + n + 1 +
23 21 22 mpan2 n + n + 1 +
24 23 relogcld n + log n + 1
25 relogcl n + log n
26 24 25 resubcld n + log n + 1 log n
27 rpre n + n
28 chpcl n ψ n
29 27 28 syl n + ψ n
30 26 29 remulcld n + log n + 1 log n ψ n
31 30 recnd n + log n + 1 log n ψ n
32 20 31 syl x + n 1 x log n + 1 log n ψ n
33 17 32 fsumcl x + n = 1 x log n + 1 log n ψ n
34 rpcnne0 x + x x 0
35 divsubdir ψ x log x + 1 log x n = 1 x log n + 1 log n ψ n x x 0 ψ x log x + 1 log x n = 1 x log n + 1 log n ψ n x = ψ x log x + 1 log x x n = 1 x log n + 1 log n ψ n x
36 16 33 34 35 syl3anc x + ψ x log x + 1 log x n = 1 x log n + 1 log n ψ n x = ψ x log x + 1 log x x n = 1 x log n + 1 log n ψ n x
37 4 12 mulcld x + ψ x log x + 1
38 4 14 mulcld x + ψ x log x
39 37 38 33 sub32d x + ψ x log x + 1 - ψ x log x - n = 1 x log n + 1 log n ψ n = ψ x log x + 1 - n = 1 x log n + 1 log n ψ n - ψ x log x
40 4 12 14 subdid x + ψ x log x + 1 log x = ψ x log x + 1 ψ x log x
41 40 oveq1d x + ψ x log x + 1 log x n = 1 x log n + 1 log n ψ n = ψ x log x + 1 - ψ x log x - n = 1 x log n + 1 log n ψ n
42 fveq2 m = n log m = log n
43 fvoveq1 m = n ψ m 1 = ψ n 1
44 42 43 jca m = n log m = log n ψ m 1 = ψ n 1
45 fveq2 m = n + 1 log m = log n + 1
46 fvoveq1 m = n + 1 ψ m 1 = ψ n + 1 - 1
47 45 46 jca m = n + 1 log m = log n + 1 ψ m 1 = ψ n + 1 - 1
48 fveq2 m = 1 log m = log 1
49 log1 log 1 = 0
50 48 49 syl6eq m = 1 log m = 0
51 oveq1 m = 1 m 1 = 1 1
52 1m1e0 1 1 = 0
53 51 52 syl6eq m = 1 m 1 = 0
54 53 fveq2d m = 1 ψ m 1 = ψ 0
55 2pos 0 < 2
56 0re 0
57 chpeq0 0 ψ 0 = 0 0 < 2
58 56 57 ax-mp ψ 0 = 0 0 < 2
59 55 58 mpbir ψ 0 = 0
60 54 59 syl6eq m = 1 ψ m 1 = 0
61 50 60 jca m = 1 log m = 0 ψ m 1 = 0
62 fveq2 m = x + 1 log m = log x + 1
63 fvoveq1 m = x + 1 ψ m 1 = ψ x + 1 - 1
64 62 63 jca m = x + 1 log m = log x + 1 ψ m 1 = ψ x + 1 - 1
65 nnuz = 1
66 9 65 eleqtrdi x + x + 1 1
67 elfznn m 1 x + 1 m
68 67 adantl x + m 1 x + 1 m
69 68 nnrpd x + m 1 x + 1 m +
70 69 relogcld x + m 1 x + 1 log m
71 70 recnd x + m 1 x + 1 log m
72 68 nnred x + m 1 x + 1 m
73 peano2rem m m 1
74 72 73 syl x + m 1 x + 1 m 1
75 chpcl m 1 ψ m 1
76 74 75 syl x + m 1 x + 1 ψ m 1
77 76 recnd x + m 1 x + 1 ψ m 1
78 44 47 61 64 66 71 77 fsumparts x + n 1 ..^ x + 1 log n ψ n + 1 - 1 ψ n 1 = log x + 1 ψ x + 1 - 1 - 0 0 - n 1 ..^ x + 1 log n + 1 log n ψ n + 1 - 1
79 7 nn0zd x + x
80 fzval3 x 1 x = 1 ..^ x + 1
81 79 80 syl x + 1 x = 1 ..^ x + 1
82 81 eqcomd x + 1 ..^ x + 1 = 1 x
83 nnm1nn0 n n 1 0
84 19 83 syl x + n 1 x n 1 0
85 84 nn0red x + n 1 x n 1
86 chpcl n 1 ψ n 1
87 85 86 syl x + n 1 x ψ n 1
88 87 recnd x + n 1 x ψ n 1
89 vmacl n Λ n
90 19 89 syl x + n 1 x Λ n
91 90 recnd x + n 1 x Λ n
92 19 nncnd x + n 1 x n
93 ax-1cn 1
94 pncan n 1 n + 1 - 1 = n
95 92 93 94 sylancl x + n 1 x n + 1 - 1 = n
96 npcan n 1 n - 1 + 1 = n
97 92 93 96 sylancl x + n 1 x n - 1 + 1 = n
98 95 97 eqtr4d x + n 1 x n + 1 - 1 = n - 1 + 1
99 98 fveq2d x + n 1 x ψ n + 1 - 1 = ψ n - 1 + 1
100 chpp1 n 1 0 ψ n - 1 + 1 = ψ n 1 + Λ n - 1 + 1
101 84 100 syl x + n 1 x ψ n - 1 + 1 = ψ n 1 + Λ n - 1 + 1
102 97 fveq2d x + n 1 x Λ n - 1 + 1 = Λ n
103 102 oveq2d x + n 1 x ψ n 1 + Λ n - 1 + 1 = ψ n 1 + Λ n
104 99 101 103 3eqtrd x + n 1 x ψ n + 1 - 1 = ψ n 1 + Λ n
105 88 91 104 mvrladdd x + n 1 x ψ n + 1 - 1 ψ n 1 = Λ n
106 105 oveq2d x + n 1 x log n ψ n + 1 - 1 ψ n 1 = log n Λ n
107 20 relogcld x + n 1 x log n
108 107 recnd x + n 1 x log n
109 91 108 mulcomd x + n 1 x Λ n log n = log n Λ n
110 106 109 eqtr4d x + n 1 x log n ψ n + 1 - 1 ψ n 1 = Λ n log n
111 82 110 sumeq12rdv x + n 1 ..^ x + 1 log n ψ n + 1 - 1 ψ n 1 = n = 1 x Λ n log n
112 7 nn0cnd x + x
113 pncan x 1 x + 1 - 1 = x
114 112 93 113 sylancl x + x + 1 - 1 = x
115 114 fveq2d x + ψ x + 1 - 1 = ψ x
116 chpfl x ψ x = ψ x
117 1 116 syl x + ψ x = ψ x
118 115 117 eqtrd x + ψ x + 1 - 1 = ψ x
119 118 oveq2d x + log x + 1 ψ x + 1 - 1 = log x + 1 ψ x
120 12 4 mulcomd x + log x + 1 ψ x = ψ x log x + 1
121 119 120 eqtrd x + log x + 1 ψ x + 1 - 1 = ψ x log x + 1
122 0cn 0
123 122 mul01i 0 0 = 0
124 123 a1i x + 0 0 = 0
125 121 124 oveq12d x + log x + 1 ψ x + 1 - 1 0 0 = ψ x log x + 1 0
126 37 subid1d x + ψ x log x + 1 0 = ψ x log x + 1
127 125 126 eqtrd x + log x + 1 ψ x + 1 - 1 0 0 = ψ x log x + 1
128 95 fveq2d x + n 1 x ψ n + 1 - 1 = ψ n
129 128 oveq2d x + n 1 x log n + 1 log n ψ n + 1 - 1 = log n + 1 log n ψ n
130 82 129 sumeq12rdv x + n 1 ..^ x + 1 log n + 1 log n ψ n + 1 - 1 = n = 1 x log n + 1 log n ψ n
131 127 130 oveq12d x + log x + 1 ψ x + 1 - 1 - 0 0 - n 1 ..^ x + 1 log n + 1 log n ψ n + 1 - 1 = ψ x log x + 1 n = 1 x log n + 1 log n ψ n
132 78 111 131 3eqtr3d x + n = 1 x Λ n log n = ψ x log x + 1 n = 1 x log n + 1 log n ψ n
133 132 oveq1d x + n = 1 x Λ n log n ψ x log x = ψ x log x + 1 - n = 1 x log n + 1 log n ψ n - ψ x log x
134 39 41 133 3eqtr4d x + ψ x log x + 1 log x n = 1 x log n + 1 log n ψ n = n = 1 x Λ n log n ψ x log x
135 134 oveq1d x + ψ x log x + 1 log x n = 1 x log n + 1 log n ψ n x = n = 1 x Λ n log n ψ x log x x
136 div23 ψ x log x + 1 log x x x 0 ψ x log x + 1 log x x = ψ x x log x + 1 log x
137 4 15 34 136 syl3anc x + ψ x log x + 1 log x x = ψ x x log x + 1 log x
138 137 oveq1d x + ψ x log x + 1 log x x n = 1 x log n + 1 log n ψ n x = ψ x x log x + 1 log x n = 1 x log n + 1 log n ψ n x
139 36 135 138 3eqtr3rd x + ψ x x log x + 1 log x n = 1 x log n + 1 log n ψ n x = n = 1 x Λ n log n ψ x log x x
140 139 mpteq2ia x + ψ x x log x + 1 log x n = 1 x log n + 1 log n ψ n x = x + n = 1 x Λ n log n ψ x log x x
141 ovexd x + ψ x x log x + 1 log x V
142 ovexd x + n = 1 x log n + 1 log n ψ n x V
143 reex V
144 rpssre +
145 143 144 ssexi + V
146 145 a1i + V
147 ovexd x + ψ x x V
148 15 adantl x + log x + 1 log x
149 eqidd x + ψ x x = x + ψ x x
150 eqidd x + log x + 1 log x = x + log x + 1 log x
151 146 147 148 149 150 offval2 x + ψ x x × f x + log x + 1 log x = x + ψ x x log x + 1 log x
152 chpo1ub x + ψ x x 𝑂1
153 0red 0
154 1red 1
155 divrcnv 1 x + 1 x 0
156 93 155 mp1i x + 1 x 0
157 rpreccl x + 1 x +
158 157 rpred x + 1 x
159 158 adantl x + 1 x
160 11 13 resubcld x + log x + 1 log x
161 160 adantl x + log x + 1 log x
162 rpaddcl x + 1 + x + 1 +
163 21 162 mpan2 x + x + 1 +
164 163 relogcld x + log x + 1
165 164 13 resubcld x + log x + 1 log x
166 7 nn0red x + x
167 1red x + 1
168 flle x x x
169 1 168 syl x + x x
170 166 1 167 169 leadd1dd x + x + 1 x + 1
171 10 163 logled x + x + 1 x + 1 log x + 1 log x + 1
172 170 171 mpbid x + log x + 1 log x + 1
173 11 164 13 172 lesub1dd x + log x + 1 log x log x + 1 log x
174 logdifbnd x + log x + 1 log x 1 x
175 160 165 158 173 174 letrd x + log x + 1 log x 1 x
176 175 ad2antrl x + 1 x log x + 1 log x 1 x
177 fllep1 x x x + 1
178 1 177 syl x + x x + 1
179 logleb x + x + 1 + x x + 1 log x log x + 1
180 10 179 mpdan x + x x + 1 log x log x + 1
181 178 180 mpbid x + log x log x + 1
182 11 13 subge0d x + 0 log x + 1 log x log x log x + 1
183 181 182 mpbird x + 0 log x + 1 log x
184 183 ad2antrl x + 1 x 0 log x + 1 log x
185 153 154 156 159 161 176 184 rlimsqz2 x + log x + 1 log x 0
186 rlimo1 x + log x + 1 log x 0 x + log x + 1 log x 𝑂1
187 185 186 syl x + log x + 1 log x 𝑂1
188 o1mul x + ψ x x 𝑂1 x + log x + 1 log x 𝑂1 x + ψ x x × f x + log x + 1 log x 𝑂1
189 152 187 188 sylancr x + ψ x x × f x + log x + 1 log x 𝑂1
190 151 189 eqeltrrd x + ψ x x log x + 1 log x 𝑂1
191 nnrp m m +
192 191 ssriv +
193 192 a1i +
194 193 sselda n n +
195 194 31 syl n log n + 1 log n ψ n
196 chpo1ub n + ψ n n 𝑂1
197 196 a1i n + ψ n n 𝑂1
198 rerpdivcl ψ n n + ψ n n
199 29 198 mpancom n + ψ n n
200 199 adantl n + ψ n n
201 31 adantl n + log n + 1 log n ψ n
202 rpreccl n + 1 n +
203 202 rpred n + 1 n
204 chpge0 n 0 ψ n
205 27 204 syl n + 0 ψ n
206 logdifbnd n + log n + 1 log n 1 n
207 26 203 29 205 206 lemul1ad n + log n + 1 log n ψ n 1 n ψ n
208 27 lep1d n + n n + 1
209 logleb n + n + 1 + n n + 1 log n log n + 1
210 23 209 mpdan n + n n + 1 log n log n + 1
211 208 210 mpbid n + log n log n + 1
212 24 25 subge0d n + 0 log n + 1 log n log n log n + 1
213 211 212 mpbird n + 0 log n + 1 log n
214 26 29 213 205 mulge0d n + 0 log n + 1 log n ψ n
215 30 214 absidd n + log n + 1 log n ψ n = log n + 1 log n ψ n
216 rpregt0 n + n 0 < n
217 divge0 ψ n 0 ψ n n 0 < n 0 ψ n n
218 29 205 216 217 syl21anc n + 0 ψ n n
219 199 218 absidd n + ψ n n = ψ n n
220 29 recnd n + ψ n
221 rpcn n + n
222 rpne0 n + n 0
223 220 221 222 divrec2d n + ψ n n = 1 n ψ n
224 219 223 eqtrd n + ψ n n = 1 n ψ n
225 207 215 224 3brtr4d n + log n + 1 log n ψ n ψ n n
226 225 ad2antrl n + 1 n log n + 1 log n ψ n ψ n n
227 154 197 200 201 226 o1le n + log n + 1 log n ψ n 𝑂1
228 193 227 o1res2 n log n + 1 log n ψ n 𝑂1
229 195 228 o1fsum x + n = 1 x log n + 1 log n ψ n x 𝑂1
230 141 142 190 229 o1sub2 x + ψ x x log x + 1 log x n = 1 x log n + 1 log n ψ n x 𝑂1
231 140 230 eqeltrrid x + n = 1 x Λ n log n ψ x log x x 𝑂1
232 231 mptru x + n = 1 x Λ n log n ψ x log x x 𝑂1