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