Metamath Proof Explorer


Theorem selberglem2

Description: Lemma for selberg . (Contributed by Mario Carneiro, 23-May-2016)

Ref Expression
Hypothesis selberglem1.t T = log x n 2 + 2 - 2 log x n n
Assertion selberglem2 x + n = 1 x m = 1 x n μ n log m 2 x 2 log x 𝑂1

Proof

Step Hyp Ref Expression
1 selberglem1.t T = log x n 2 + 2 - 2 log x n n
2 reex V
3 rpssre +
4 2 3 ssexi + V
5 4 a1i + V
6 fzfid x + 1 x Fin
7 elfznn n 1 x n
8 7 adantl x + n 1 x n
9 mucl n μ n
10 8 9 syl x + n 1 x μ n
11 10 zred x + n 1 x μ n
12 11 recnd x + n 1 x μ n
13 fzfid x + n 1 x 1 x n Fin
14 elfznn m 1 x n m
15 14 adantl x + n 1 x m 1 x n m
16 15 nnrpd x + n 1 x m 1 x n m +
17 16 relogcld x + n 1 x m 1 x n log m
18 17 resqcld x + n 1 x m 1 x n log m 2
19 13 18 fsumrecl x + n 1 x m = 1 x n log m 2
20 simplr x + n 1 x x +
21 19 20 rerpdivcld x + n 1 x m = 1 x n log m 2 x
22 21 recnd x + n 1 x m = 1 x n log m 2 x
23 simpr x + x +
24 7 nnrpd n 1 x n +
25 rpdivcl x + n + x n +
26 23 24 25 syl2an x + n 1 x x n +
27 26 relogcld x + n 1 x log x n
28 27 resqcld x + n 1 x log x n 2
29 2re 2
30 remulcl 2 log x n 2 log x n
31 29 27 30 sylancr x + n 1 x 2 log x n
32 resubcl 2 2 log x n 2 2 log x n
33 29 31 32 sylancr x + n 1 x 2 2 log x n
34 28 33 readdcld x + n 1 x log x n 2 + 2 - 2 log x n
35 34 8 nndivred x + n 1 x log x n 2 + 2 - 2 log x n n
36 1 35 eqeltrid x + n 1 x T
37 36 recnd x + n 1 x T
38 22 37 subcld x + n 1 x m = 1 x n log m 2 x T
39 12 38 mulcld x + n 1 x μ n m = 1 x n log m 2 x T
40 6 39 fsumcl x + n = 1 x μ n m = 1 x n log m 2 x T
41 12 37 mulcld x + n 1 x μ n T
42 6 41 fsumcl x + n = 1 x μ n T
43 2cn 2
44 relogcl x + log x
45 44 adantl x + log x
46 45 recnd x + log x
47 mulcl 2 log x 2 log x
48 43 46 47 sylancr x + 2 log x
49 42 48 subcld x + n = 1 x μ n T 2 log x
50 eqidd x + n = 1 x μ n m = 1 x n log m 2 x T = x + n = 1 x μ n m = 1 x n log m 2 x T
51 eqidd x + n = 1 x μ n T 2 log x = x + n = 1 x μ n T 2 log x
52 5 40 49 50 51 offval2 x + n = 1 x μ n m = 1 x n log m 2 x T + f x + n = 1 x μ n T 2 log x = x + n = 1 x μ n m = 1 x n log m 2 x T + n = 1 x μ n T - 2 log x
53 40 42 48 addsubassd x + n = 1 x μ n m = 1 x n log m 2 x T + n = 1 x μ n T - 2 log x = n = 1 x μ n m = 1 x n log m 2 x T + n = 1 x μ n T - 2 log x
54 rpcnne0 x + x x 0
55 54 adantl x + x x 0
56 55 simpld x + x
57 11 adantr x + n 1 x m 1 x n μ n
58 57 18 remulcld x + n 1 x m 1 x n μ n log m 2
59 13 58 fsumrecl x + n 1 x m = 1 x n μ n log m 2
60 59 recnd x + n 1 x m = 1 x n μ n log m 2
61 55 simprd x + x 0
62 6 56 60 61 fsumdivc x + n = 1 x m = 1 x n μ n log m 2 x = n = 1 x m = 1 x n μ n log m 2 x
63 18 recnd x + n 1 x m 1 x n log m 2
64 13 63 fsumcl x + n 1 x m = 1 x n log m 2
65 55 adantr x + n 1 x x x 0
66 divass μ n m = 1 x n log m 2 x x 0 μ n m = 1 x n log m 2 x = μ n m = 1 x n log m 2 x
67 12 64 65 66 syl3anc x + n 1 x μ n m = 1 x n log m 2 x = μ n m = 1 x n log m 2 x
68 13 12 63 fsummulc2 x + n 1 x μ n m = 1 x n log m 2 = m = 1 x n μ n log m 2
69 68 oveq1d x + n 1 x μ n m = 1 x n log m 2 x = m = 1 x n μ n log m 2 x
70 22 37 npcand x + n 1 x m = 1 x n log m 2 x - T + T = m = 1 x n log m 2 x
71 70 oveq2d x + n 1 x μ n m = 1 x n log m 2 x - T + T = μ n m = 1 x n log m 2 x
72 12 38 37 adddid x + n 1 x μ n m = 1 x n log m 2 x - T + T = μ n m = 1 x n log m 2 x T + μ n T
73 71 72 eqtr3d x + n 1 x μ n m = 1 x n log m 2 x = μ n m = 1 x n log m 2 x T + μ n T
74 67 69 73 3eqtr3d x + n 1 x m = 1 x n μ n log m 2 x = μ n m = 1 x n log m 2 x T + μ n T
75 74 sumeq2dv x + n = 1 x m = 1 x n μ n log m 2 x = n = 1 x μ n m = 1 x n log m 2 x T + μ n T
76 6 39 41 fsumadd x + n = 1 x μ n m = 1 x n log m 2 x T + μ n T = n = 1 x μ n m = 1 x n log m 2 x T + n = 1 x μ n T
77 62 75 76 3eqtrrd x + n = 1 x μ n m = 1 x n log m 2 x T + n = 1 x μ n T = n = 1 x m = 1 x n μ n log m 2 x
78 77 oveq1d x + n = 1 x μ n m = 1 x n log m 2 x T + n = 1 x μ n T - 2 log x = n = 1 x m = 1 x n μ n log m 2 x 2 log x
79 53 78 eqtr3d x + n = 1 x μ n m = 1 x n log m 2 x T + n = 1 x μ n T - 2 log x = n = 1 x m = 1 x n μ n log m 2 x 2 log x
80 79 mpteq2dva x + n = 1 x μ n m = 1 x n log m 2 x T + n = 1 x μ n T - 2 log x = x + n = 1 x m = 1 x n μ n log m 2 x 2 log x
81 52 80 eqtrd x + n = 1 x μ n m = 1 x n log m 2 x T + f x + n = 1 x μ n T 2 log x = x + n = 1 x m = 1 x n μ n log m 2 x 2 log x
82 1red 1
83 6 28 fsumrecl x + n = 1 x log x n 2
84 83 23 rerpdivcld x + n = 1 x log x n 2 x
85 84 recnd x + n = 1 x log x n 2 x
86 2cnd x + 2
87 2nn0 2 0
88 logexprlim 2 0 x + n = 1 x log x n 2 x 2 !
89 87 88 mp1i x + n = 1 x log x n 2 x 2 !
90 2cnd 2
91 rlimconst + 2 x + 2 2
92 3 90 91 sylancr x + 2 2
93 85 86 89 92 rlimadd x + n = 1 x log x n 2 x + 2 2 ! + 2
94 rlimo1 x + n = 1 x log x n 2 x + 2 2 ! + 2 x + n = 1 x log x n 2 x + 2 𝑂1
95 93 94 syl x + n = 1 x log x n 2 x + 2 𝑂1
96 readdcl n = 1 x log x n 2 x 2 n = 1 x log x n 2 x + 2
97 84 29 96 sylancl x + n = 1 x log x n 2 x + 2
98 40 abscld x + n = 1 x μ n m = 1 x n log m 2 x T
99 97 recnd x + n = 1 x log x n 2 x + 2
100 99 abscld x + n = 1 x log x n 2 x + 2
101 39 abscld x + n 1 x μ n m = 1 x n log m 2 x T
102 6 101 fsumrecl x + n = 1 x μ n m = 1 x n log m 2 x T
103 6 39 fsumabs x + n = 1 x μ n m = 1 x n log m 2 x T n = 1 x μ n m = 1 x n log m 2 x T
104 readdcl log x n 2 2 log x n 2 + 2
105 28 29 104 sylancl x + n 1 x log x n 2 + 2
106 105 20 rerpdivcld x + n 1 x log x n 2 + 2 x
107 6 106 fsumrecl x + n = 1 x log x n 2 + 2 x
108 38 abscld x + n 1 x m = 1 x n log m 2 x T
109 12 38 absmuld x + n 1 x μ n m = 1 x n log m 2 x T = μ n m = 1 x n log m 2 x T
110 12 abscld x + n 1 x μ n
111 1red x + n 1 x 1
112 38 absge0d x + n 1 x 0 m = 1 x n log m 2 x T
113 mule1 n μ n 1
114 8 113 syl x + n 1 x μ n 1
115 110 111 108 112 114 lemul1ad x + n 1 x μ n m = 1 x n log m 2 x T 1 m = 1 x n log m 2 x T
116 108 recnd x + n 1 x m = 1 x n log m 2 x T
117 116 mulid2d x + n 1 x 1 m = 1 x n log m 2 x T = m = 1 x n log m 2 x T
118 115 117 breqtrd x + n 1 x μ n m = 1 x n log m 2 x T m = 1 x n log m 2 x T
119 109 118 eqbrtrd x + n 1 x μ n m = 1 x n log m 2 x T m = 1 x n log m 2 x T
120 65 simpld x + n 1 x x
121 120 38 absmuld x + n 1 x x m = 1 x n log m 2 x T = x m = 1 x n log m 2 x T
122 120 22 37 subdid x + n 1 x x m = 1 x n log m 2 x T = x m = 1 x n log m 2 x x T
123 65 simprd x + n 1 x x 0
124 64 120 123 divcan2d x + n 1 x x m = 1 x n log m 2 x = m = 1 x n log m 2
125 34 recnd x + n 1 x log x n 2 + 2 - 2 log x n
126 8 nnrpd x + n 1 x n +
127 rpcnne0 n + n n 0
128 126 127 syl x + n 1 x n n 0
129 divass x log x n 2 + 2 - 2 log x n n n 0 x log x n 2 + 2 - 2 log x n n = x log x n 2 + 2 - 2 log x n n
130 1 oveq2i x T = x log x n 2 + 2 - 2 log x n n
131 129 130 syl6eqr x log x n 2 + 2 - 2 log x n n n 0 x log x n 2 + 2 - 2 log x n n = x T
132 div23 x log x n 2 + 2 - 2 log x n n n 0 x log x n 2 + 2 - 2 log x n n = x n log x n 2 + 2 - 2 log x n
133 131 132 eqtr3d x log x n 2 + 2 - 2 log x n n n 0 x T = x n log x n 2 + 2 - 2 log x n
134 120 125 128 133 syl3anc x + n 1 x x T = x n log x n 2 + 2 - 2 log x n
135 124 134 oveq12d x + n 1 x x m = 1 x n log m 2 x x T = m = 1 x n log m 2 x n log x n 2 + 2 - 2 log x n
136 122 135 eqtrd x + n 1 x x m = 1 x n log m 2 x T = m = 1 x n log m 2 x n log x n 2 + 2 - 2 log x n
137 136 fveq2d x + n 1 x x m = 1 x n log m 2 x T = m = 1 x n log m 2 x n log x n 2 + 2 - 2 log x n
138 rprege0 x + x 0 x
139 absid x 0 x x = x
140 20 138 139 3syl x + n 1 x x = x
141 140 oveq1d x + n 1 x x m = 1 x n log m 2 x T = x m = 1 x n log m 2 x T
142 121 137 141 3eqtr3d x + n 1 x m = 1 x n log m 2 x n log x n 2 + 2 - 2 log x n = x m = 1 x n log m 2 x T
143 8 nncnd x + n 1 x n
144 143 mulid2d x + n 1 x 1 n = n
145 rpre x + x
146 145 adantl x + x
147 fznnfl x n 1 x n n x
148 146 147 syl x + n 1 x n n x
149 148 simplbda x + n 1 x n x
150 144 149 eqbrtrd x + n 1 x 1 n x
151 20 rpred x + n 1 x x
152 111 151 126 lemuldivd x + n 1 x 1 n x 1 x n
153 150 152 mpbid x + n 1 x 1 x n
154 log2sumbnd x n + 1 x n m = 1 x n log m 2 x n log x n 2 + 2 - 2 log x n log x n 2 + 2
155 26 153 154 syl2anc x + n 1 x m = 1 x n log m 2 x n log x n 2 + 2 - 2 log x n log x n 2 + 2
156 142 155 eqbrtrrd x + n 1 x x m = 1 x n log m 2 x T log x n 2 + 2
157 108 105 20 lemuldiv2d x + n 1 x x m = 1 x n log m 2 x T log x n 2 + 2 m = 1 x n log m 2 x T log x n 2 + 2 x
158 156 157 mpbid x + n 1 x m = 1 x n log m 2 x T log x n 2 + 2 x
159 101 108 106 119 158 letrd x + n 1 x μ n m = 1 x n log m 2 x T log x n 2 + 2 x
160 6 101 106 159 fsumle x + n = 1 x μ n m = 1 x n log m 2 x T n = 1 x log x n 2 + 2 x
161 6 105 fsumrecl x + n = 1 x log x n 2 + 2
162 remulcl x 2 x 2
163 146 29 162 sylancl x + x 2
164 83 163 readdcld x + n = 1 x log x n 2 + x 2
165 28 recnd x + n 1 x log x n 2
166 2cnd x + n 1 x 2
167 6 165 166 fsumadd x + n = 1 x log x n 2 + 2 = n = 1 x log x n 2 + n = 1 x 2
168 fsumconst 1 x Fin 2 n = 1 x 2 = 1 x 2
169 6 43 168 sylancl x + n = 1 x 2 = 1 x 2
170 138 adantl x + x 0 x
171 flge0nn0 x 0 x x 0
172 hashfz1 x 0 1 x = x
173 170 171 172 3syl x + 1 x = x
174 173 oveq1d x + 1 x 2 = x 2
175 169 174 eqtrd x + n = 1 x 2 = x 2
176 175 oveq2d x + n = 1 x log x n 2 + n = 1 x 2 = n = 1 x log x n 2 + x 2
177 167 176 eqtrd x + n = 1 x log x n 2 + 2 = n = 1 x log x n 2 + x 2
178 reflcl x x
179 146 178 syl x + x
180 29 a1i x + 2
181 179 180 remulcld x + x 2
182 flle x x x
183 146 182 syl x + x x
184 2pos 0 < 2
185 29 184 pm3.2i 2 0 < 2
186 185 a1i x + 2 0 < 2
187 lemul1 x x 2 0 < 2 x x x 2 x 2
188 179 146 186 187 syl3anc x + x x x 2 x 2
189 183 188 mpbid x + x 2 x 2
190 181 163 83 189 leadd2dd x + n = 1 x log x n 2 + x 2 n = 1 x log x n 2 + x 2
191 177 190 eqbrtrd x + n = 1 x log x n 2 + 2 n = 1 x log x n 2 + x 2
192 161 164 23 191 lediv1dd x + n = 1 x log x n 2 + 2 x n = 1 x log x n 2 + x 2 x
193 105 recnd x + n 1 x log x n 2 + 2
194 6 56 193 61 fsumdivc x + n = 1 x log x n 2 + 2 x = n = 1 x log x n 2 + 2 x
195 83 recnd x + n = 1 x log x n 2
196 56 86 mulcld x + x 2
197 divdir n = 1 x log x n 2 x 2 x x 0 n = 1 x log x n 2 + x 2 x = n = 1 x log x n 2 x + x 2 x
198 195 196 55 197 syl3anc x + n = 1 x log x n 2 + x 2 x = n = 1 x log x n 2 x + x 2 x
199 86 56 61 divcan3d x + x 2 x = 2
200 199 oveq2d x + n = 1 x log x n 2 x + x 2 x = n = 1 x log x n 2 x + 2
201 198 200 eqtrd x + n = 1 x log x n 2 + x 2 x = n = 1 x log x n 2 x + 2
202 192 194 201 3brtr3d x + n = 1 x log x n 2 + 2 x n = 1 x log x n 2 x + 2
203 102 107 97 160 202 letrd x + n = 1 x μ n m = 1 x n log m 2 x T n = 1 x log x n 2 x + 2
204 98 102 97 103 203 letrd x + n = 1 x μ n m = 1 x n log m 2 x T n = 1 x log x n 2 x + 2
205 97 leabsd x + n = 1 x log x n 2 x + 2 n = 1 x log x n 2 x + 2
206 98 97 100 204 205 letrd x + n = 1 x μ n m = 1 x n log m 2 x T n = 1 x log x n 2 x + 2
207 206 adantrr x + 1 x n = 1 x μ n m = 1 x n log m 2 x T n = 1 x log x n 2 x + 2
208 82 95 97 40 207 o1le x + n = 1 x μ n m = 1 x n log m 2 x T 𝑂1
209 1 selberglem1 x + n = 1 x μ n T 2 log x 𝑂1
210 o1add x + n = 1 x μ n m = 1 x n log m 2 x T 𝑂1 x + n = 1 x μ n T 2 log x 𝑂1 x + n = 1 x μ n m = 1 x n log m 2 x T + f x + n = 1 x μ n T 2 log x 𝑂1
211 208 209 210 sylancl x + n = 1 x μ n m = 1 x n log m 2 x T + f x + n = 1 x μ n T 2 log x 𝑂1
212 81 211 eqeltrrd x + n = 1 x m = 1 x n μ n log m 2 x 2 log x 𝑂1
213 212 mptru x + n = 1 x m = 1 x n μ n log m 2 x 2 log x 𝑂1