Metamath Proof Explorer


Theorem basellem9

Description: Lemma for basel . Since by basellem8 F is bounded by two expressions that tend to _pi ^ 2 / 6 , F must also go to _pi ^ 2 / 6 by the squeeze theorem climsqz . But the series F is exactly the partial sums of k ^ -u 2 , so it follows that this is also the value of the infinite sum sum_ k e. NN ( k ^ -u 2 ) . (Contributed by Mario Carneiro, 28-Jul-2014)

Ref Expression
Hypotheses basel.g G = n 1 2 n + 1
basel.f F = seq 1 + n n 2
basel.h H = × π 2 6 × f × 1 f G
basel.j J = H × f × 1 + f × 2 × f G
basel.k K = H × f × 1 + f G
Assertion basellem9 k k 2 = π 2 6

Proof

Step Hyp Ref Expression
1 basel.g G = n 1 2 n + 1
2 basel.f F = seq 1 + n n 2
3 basel.h H = × π 2 6 × f × 1 f G
4 basel.j J = H × f × 1 + f × 2 × f G
5 basel.k K = H × f × 1 + f G
6 nnuz = 1
7 1zzd 1
8 oveq1 n = k n 2 = k 2
9 eqid n n 2 = n n 2
10 ovex k 2 V
11 8 9 10 fvmpt k n n 2 k = k 2
12 11 adantl k n n 2 k = k 2
13 nnre n n
14 nnne0 n n 0
15 2z 2
16 znegcl 2 2
17 15 16 ax-mp 2
18 17 a1i n 2
19 13 14 18 reexpclzd n n 2
20 19 adantl n n 2
21 20 9 fmptd n n 2 :
22 21 ffvelrnda k n n 2 k
23 12 22 eqeltrrd k k 2
24 23 recnd k k 2
25 6 7 22 serfre seq 1 + n n 2 :
26 2 feq1i F : seq 1 + n n 2 :
27 25 26 sylibr F :
28 27 ffvelrnda n F n
29 28 recnd n F n
30 remulcl x y x y
31 30 adantl x y x y
32 ovex π 2 6 V
33 32 fconst × π 2 6 : π 2 6
34 pire π
35 34 resqcli π 2
36 6re 6
37 6nn 6
38 37 nnne0i 6 0
39 35 36 38 redivcli π 2 6
40 39 a1i π 2 6
41 40 snssd π 2 6
42 fss × π 2 6 : π 2 6 π 2 6 × π 2 6 :
43 33 41 42 sylancr × π 2 6 :
44 resubcl x y x y
45 44 adantl x y x y
46 1ex 1 V
47 46 fconst × 1 : 1
48 1red 1
49 48 snssd 1
50 fss × 1 : 1 1 × 1 :
51 47 49 50 sylancr × 1 :
52 2nn 2
53 52 a1i 2
54 nnmulcl 2 n 2 n
55 53 54 sylan n 2 n
56 55 peano2nnd n 2 n + 1
57 56 nnrecred n 1 2 n + 1
58 57 1 fmptd G :
59 nnex V
60 59 a1i V
61 inidm =
62 45 51 58 60 60 61 off × 1 f G :
63 31 43 62 60 60 61 off × π 2 6 × f × 1 f G :
64 3 feq1i H : × π 2 6 × f × 1 f G :
65 63 64 sylibr H :
66 readdcl x y x + y
67 66 adantl x y x + y
68 negex 2 V
69 68 fconst × 2 : 2
70 17 zrei 2
71 70 a1i 2
72 71 snssd 2
73 fss × 2 : 2 2 × 2 :
74 69 72 73 sylancr × 2 :
75 31 74 58 60 60 61 off × 2 × f G :
76 67 51 75 60 60 61 off × 1 + f × 2 × f G :
77 31 65 76 60 60 61 off H × f × 1 + f × 2 × f G :
78 4 feq1i J : H × f × 1 + f × 2 × f G :
79 77 78 sylibr J :
80 79 ffvelrnda n J n
81 80 recnd n J n
82 29 81 npcand n F n - J n + J n = F n
83 82 mpteq2dva n F n - J n + J n = n F n
84 ovexd n F n J n V
85 27 feqmptd F = n F n
86 79 feqmptd J = n J n
87 60 28 80 85 86 offval2 F f J = n F n J n
88 60 84 80 87 86 offval2 F f J + f J = n F n - J n + J n
89 83 88 85 3eqtr4d F f J + f J = F
90 67 51 58 60 60 61 off × 1 + f G :
91 recn x x
92 recn y y
93 recn z z
94 subdi x y z x y z = x y x z
95 91 92 93 94 syl3an x y z x y z = x y x z
96 95 adantl x y z x y z = x y x z
97 60 65 90 76 96 caofdi H × f × 1 + f G f × 1 + f × 2 × f G = H × f × 1 + f G f H × f × 1 + f × 2 × f G
98 5 4 oveq12i K f J = H × f × 1 + f G f H × f × 1 + f × 2 × f G
99 97 98 eqtr4di H × f × 1 + f G f × 1 + f × 2 × f G = K f J
100 39 recni π 2 6
101 6 eqimss2i 1
102 101 59 climconst2 π 2 6 1 × π 2 6 π 2 6
103 100 7 102 sylancr × π 2 6 π 2 6
104 ovexd × π 2 6 × f × 1 f G V
105 ax-resscn
106 fss × 1 : × 1 :
107 51 105 106 sylancl × 1 :
108 fss G : G :
109 58 105 108 sylancl G :
110 ofnegsub V × 1 : G : × 1 + f × 1 × f G = × 1 f G
111 59 107 109 110 mp3an2i × 1 + f × 1 × f G = × 1 f G
112 neg1cn 1
113 1 112 basellem7 × 1 + f × 1 × f G 1
114 111 113 eqbrtrrdi × 1 f G 1
115 43 ffvelrnda k × π 2 6 k
116 115 recnd k × π 2 6 k
117 62 ffvelrnda k × 1 f G k
118 117 recnd k × 1 f G k
119 43 ffnd × π 2 6 Fn
120 fnconstg 1 × 1 Fn
121 7 120 syl × 1 Fn
122 58 ffnd G Fn
123 121 122 60 60 61 offn × 1 f G Fn
124 eqidd k × π 2 6 k = × π 2 6 k
125 eqidd k × 1 f G k = × 1 f G k
126 119 123 60 60 61 124 125 ofval k × π 2 6 × f × 1 f G k = × π 2 6 k × 1 f G k
127 6 7 103 104 114 116 118 126 climmul × π 2 6 × f × 1 f G π 2 6 1
128 100 mulid1i π 2 6 1 = π 2 6
129 127 128 breqtrdi × π 2 6 × f × 1 f G π 2 6
130 3 129 eqbrtrid H π 2 6
131 ovexd H × f × 1 + f G f × 1 + f × 2 × f G V
132 3cn 3
133 101 59 climconst2 3 1 × 3 3
134 132 7 133 sylancr × 3 3
135 ovexd × 3 × f G V
136 1 basellem6 G 0
137 136 a1i G 0
138 3ex 3 V
139 138 fconst × 3 : 3
140 3re 3
141 140 a1i 3
142 141 snssd 3
143 fss × 3 : 3 3 × 3 :
144 139 142 143 sylancr × 3 :
145 144 ffvelrnda k × 3 k
146 145 recnd k × 3 k
147 58 ffvelrnda k G k
148 147 recnd k G k
149 144 ffnd × 3 Fn
150 eqidd k × 3 k = × 3 k
151 eqidd k G k = G k
152 149 122 60 60 61 150 151 ofval k × 3 × f G k = × 3 k G k
153 6 7 134 135 137 146 148 152 climmul × 3 × f G 3 0
154 132 mul01i 3 0 = 0
155 153 154 breqtrdi × 3 × f G 0
156 65 ffvelrnda k H k
157 156 recnd k H k
158 31 144 58 60 60 61 off × 3 × f G :
159 158 ffvelrnda k × 3 × f G k
160 159 recnd k × 3 × f G k
161 65 ffnd H Fn
162 45 90 76 60 60 61 off × 1 + f G f × 1 + f × 2 × f G :
163 162 ffnd × 1 + f G f × 1 + f × 2 × f G Fn
164 eqidd k H k = H k
165 148 mulid2d k 1 G k = G k
166 2cn 2
167 mulneg1 2 G k -2 G k = 2 G k
168 166 148 167 sylancr k -2 G k = 2 G k
169 168 negeqd k -2 G k = 2 G k
170 mulcl 2 G k 2 G k
171 166 148 170 sylancr k 2 G k
172 171 negnegd k 2 G k = 2 G k
173 169 172 eqtr2d k 2 G k = -2 G k
174 165 173 oveq12d k 1 G k + 2 G k = G k + -2 G k
175 remulcl 2 G k -2 G k
176 70 147 175 sylancr k -2 G k
177 176 recnd k -2 G k
178 148 177 negsubd k G k + -2 G k = G k -2 G k
179 174 178 eqtrd k 1 G k + 2 G k = G k -2 G k
180 df-3 3 = 2 + 1
181 ax-1cn 1
182 166 181 addcomi 2 + 1 = 1 + 2
183 180 182 eqtri 3 = 1 + 2
184 183 oveq1i 3 G k = 1 + 2 G k
185 1cnd k 1
186 166 a1i k 2
187 185 186 148 adddird k 1 + 2 G k = 1 G k + 2 G k
188 184 187 syl5eq k 3 G k = 1 G k + 2 G k
189 185 148 177 pnpcand k 1 + G k - 1 + -2 G k = G k -2 G k
190 179 188 189 3eqtr4rd k 1 + G k - 1 + -2 G k = 3 G k
191 121 122 60 60 61 offn × 1 + f G Fn
192 17 a1i 2
193 fnconstg 2 × 2 Fn
194 192 193 syl × 2 Fn
195 194 122 60 60 61 offn × 2 × f G Fn
196 121 195 60 60 61 offn × 1 + f × 2 × f G Fn
197 60 48 122 151 ofc1 k × 1 + f G k = 1 + G k
198 60 71 122 151 ofc1 k × 2 × f G k = -2 G k
199 60 48 195 198 ofc1 k × 1 + f × 2 × f G k = 1 + -2 G k
200 191 196 60 60 61 197 199 ofval k × 1 + f G f × 1 + f × 2 × f G k = 1 + G k - 1 + -2 G k
201 60 141 122 151 ofc1 k × 3 × f G k = 3 G k
202 190 200 201 3eqtr4d k × 1 + f G f × 1 + f × 2 × f G k = × 3 × f G k
203 161 163 60 60 61 164 202 ofval k H × f × 1 + f G f × 1 + f × 2 × f G k = H k × 3 × f G k
204 6 7 130 131 155 157 160 203 climmul H × f × 1 + f G f × 1 + f × 2 × f G π 2 6 0
205 100 mul01i π 2 6 0 = 0
206 204 205 breqtrdi H × f × 1 + f G f × 1 + f × 2 × f G 0
207 99 206 eqbrtrrd K f J 0
208 ovexd F f J V
209 31 65 90 60 60 61 off H × f × 1 + f G :
210 5 feq1i K : H × f × 1 + f G :
211 209 210 sylibr K :
212 45 211 79 60 60 61 off K f J :
213 212 ffvelrnda k K f J k
214 45 27 79 60 60 61 off F f J :
215 214 ffvelrnda k F f J k
216 27 ffvelrnda k F k
217 211 ffvelrnda k K k
218 79 ffvelrnda k J k
219 eqid 2 k + 1 = 2 k + 1
220 1 2 3 4 5 219 basellem8 k J k F k F k K k
221 220 adantl k J k F k F k K k
222 221 simprd k F k K k
223 216 217 218 222 lesub1dd k F k J k K k J k
224 27 ffnd F Fn
225 79 ffnd J Fn
226 eqidd k F k = F k
227 eqidd k J k = J k
228 224 225 60 60 61 226 227 ofval k F f J k = F k J k
229 211 ffnd K Fn
230 eqidd k K k = K k
231 229 225 60 60 61 230 227 ofval k K f J k = K k J k
232 223 228 231 3brtr4d k F f J k K f J k
233 221 simpld k J k F k
234 216 218 subge0d k 0 F k J k J k F k
235 233 234 mpbird k 0 F k J k
236 235 228 breqtrrd k 0 F f J k
237 6 7 207 208 213 215 232 236 climsqz2 F f J 0
238 ovexd F f J + f J V
239 ovexd H × f × 1 + f × 2 × f G V
240 70 recni 2
241 1 240 basellem7 × 1 + f × 2 × f G 1
242 241 a1i × 1 + f × 2 × f G 1
243 76 ffvelrnda k × 1 + f × 2 × f G k
244 243 recnd k × 1 + f × 2 × f G k
245 eqidd k × 1 + f × 2 × f G k = × 1 + f × 2 × f G k
246 161 196 60 60 61 164 245 ofval k H × f × 1 + f × 2 × f G k = H k × 1 + f × 2 × f G k
247 6 7 130 239 242 157 244 246 climmul H × f × 1 + f × 2 × f G π 2 6 1
248 247 128 breqtrdi H × f × 1 + f × 2 × f G π 2 6
249 4 248 eqbrtrid J π 2 6
250 215 recnd k F f J k
251 218 recnd k J k
252 214 ffnd F f J Fn
253 eqidd k F f J k = F f J k
254 252 225 60 60 61 253 227 ofval k F f J + f J k = F f J k + J k
255 6 7 237 238 249 250 251 254 climadd F f J + f J 0 + π 2 6
256 89 255 eqbrtrrd F 0 + π 2 6
257 100 addid2i 0 + π 2 6 = π 2 6
258 256 2 257 3brtr3g seq 1 + n n 2 π 2 6
259 6 7 12 24 258 isumclim k k 2 = π 2 6
260 259 mptru k k 2 = π 2 6