Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  esumpcvgval Unicode version

Theorem esumpcvgval 23448
 Description: The value of the extended sum when the corresponding series sum is convergent. (Contributed by Thierry Arnoux, 31-Jul-2017.)
Hypotheses
Ref Expression
esumpcvgval.1
esumpcvgval.2
esumpcvgval.3
Assertion
Ref Expression
esumpcvgval Σ*
Distinct variable groups:   ,,   ,,   ,,   ,,
Allowed substitution hints:   ()   ()   ()

Proof of Theorem esumpcvgval
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 xrltso 10477 . . . 4
21a1i 10 . . 3
3 nnuz 10265 . . . . 5
4 1z 10055 . . . . . 6
54a1i 10 . . . . 5
6 esumpcvgval.2 . . . . . . . . . 10
7 eqcom 2287 . . . . . . . . . . . 12
87imbi1i 315 . . . . . . . . . . 11
9 eqcom 2287 . . . . . . . . . . . 12
109imbi2i 303 . . . . . . . . . . 11
118, 10bitri 240 . . . . . . . . . 10
126, 11mpbi 199 . . . . . . . . 9
1312cbvmptv 4113 . . . . . . . 8
1413eqcomi 2289 . . . . . . 7
15 seqeq3 11053 . . . . . . 7
1614, 15ax-mp 8 . . . . . 6
17 esumpcvgval.1 . . . . . . . . . . 11
1817, 13fmptd 5686 . . . . . . . . . 10
1918ffvelrnda 5667 . . . . . . . . 9
20 elrege0 10748 . . . . . . . . . 10
2120simplbi 446 . . . . . . . . 9
2219, 21syl 15 . . . . . . . 8
23 readdcl 8822 . . . . . . . . 9
2423adantl 452 . . . . . . . 8
253, 5, 22, 24seqf 11069 . . . . . . 7
2618adantr 451 . . . . . . . . . . 11
27 simpr 447 . . . . . . . . . . . 12
2827peano2nnd 9765 . . . . . . . . . . 11
2926, 28ffvelrnd 5668 . . . . . . . . . 10
30 elrege0 10748 . . . . . . . . . . 11
3130simprbi 450 . . . . . . . . . 10
3229, 31syl 15 . . . . . . . . 9
3325ffvelrnda 5667 . . . . . . . . . 10
3430simplbi 446 . . . . . . . . . . 11
3529, 34syl 15 . . . . . . . . . 10
3633, 35addge01d 9362 . . . . . . . . 9
3732, 36mpbid 201 . . . . . . . 8
3827, 3syl6eleq 2375 . . . . . . . . 9
39 seqp1 11063 . . . . . . . . 9
4038, 39syl 15 . . . . . . . 8
4137, 40breqtrrd 4051 . . . . . . 7
42 simpr 447 . . . . . . . . . . 11
4313fvmpt2 5610 . . . . . . . . . . 11
4442, 17, 43syl2anc 642 . . . . . . . . . 10
45 mnfxr 10458 . . . . . . . . . . . . . 14
46 pnfxr 10457 . . . . . . . . . . . . . 14
47 0re 8840 . . . . . . . . . . . . . . 15
48 mnflt 10466 . . . . . . . . . . . . . . 15
4947, 48ax-mp 8 . . . . . . . . . . . . . 14
50 pnfge 10471 . . . . . . . . . . . . . . 15
5146, 50ax-mp 8 . . . . . . . . . . . . . 14
52 icossioo 23264 . . . . . . . . . . . . . 14
5345, 46, 49, 51, 52mp4an 654 . . . . . . . . . . . . 13
54 ioomax 10726 . . . . . . . . . . . . 13
5553, 54sseqtri 3212 . . . . . . . . . . . 12
5655, 17sseldi 3180 . . . . . . . . . . 11
5756recnd 8863 . . . . . . . . . 10
5825feqmptd 5577 . . . . . . . . . . . 12
59 simpll 730 . . . . . . . . . . . . . . . 16
60 elfznn 10821 . . . . . . . . . . . . . . . . 17
6160adantl 452 . . . . . . . . . . . . . . . 16
6259, 61, 44syl2anc 642 . . . . . . . . . . . . . . 15
6359, 61, 57syl2anc 642 . . . . . . . . . . . . . . 15
6462, 38, 63fsumser 12205 . . . . . . . . . . . . . 14
6564eqcomd 2290 . . . . . . . . . . . . 13
6665mpteq2dva 4108 . . . . . . . . . . . 12
6758, 66eqtr2d 2318 . . . . . . . . . . 11
68 esumpcvgval.3 . . . . . . . . . . 11
6967, 68eqeltrrd 2360 . . . . . . . . . 10
703, 5, 44, 57, 69isumclim2 12223 . . . . . . . . 9
713, 5, 70, 33climrecl 12059 . . . . . . . 8
724a1i 10 . . . . . . . . . . 11
73 fzfid 11037 . . . . . . . . . . 11
74 fzssuz 10834 . . . . . . . . . . . . 13
7574, 3sseqtr4i 3213 . . . . . . . . . . . 12
7675a1i 10 . . . . . . . . . . 11
7744adantlr 695 . . . . . . . . . . 11
7856adantlr 695 . . . . . . . . . . 11
7917adantlr 695 . . . . . . . . . . . 12
80 elrege0 10748 . . . . . . . . . . . . 13
8180simprbi 450 . . . . . . . . . . . 12
8279, 81syl 15 . . . . . . . . . . 11
8369adantr 451 . . . . . . . . . . 11
843, 72, 73, 76, 77, 78, 82, 83isumless 12306 . . . . . . . . . 10
8565, 84eqbrtrd 4045 . . . . . . . . 9
8685ralrimiva 2628 . . . . . . . 8
87 breq2 4029 . . . . . . . . . 10
8887ralbidv 2565 . . . . . . . . 9
8988rspcev 2886 . . . . . . . 8
9071, 86, 89syl2anc 642 . . . . . . 7
913, 5, 25, 41, 90climsup 12145 . . . . . 6
9216, 91syl5eqbr 4058 . . . . 5
93 eqid 2285 . . . . . . . . 9
9456, 93fmptd 5686 . . . . . . . 8
9594ffvelrnda 5667 . . . . . . 7
9624caovclg 6014 . . . . . . 7
973, 5, 95, 96seqf 11069 . . . . . 6
9897ffvelrnda 5667 . . . . 5
993, 5, 92, 98climrecl 12059 . . . 4
10099rexrd 8883 . . 3
101 eqid 2285 . . . . . . 7
102 sumex 12162 . . . . . . 7
103101, 102elrnmpti 4932 . . . . . 6
104 ssnnssfz 23279 . . . . . . . . . 10
105 fzfid 11037 . . . . . . . . . . . . . . 15
106105adantr 451 . . . . . . . . . . . . . 14
107 elfznn 10821 . . . . . . . . . . . . . . . . . 18
108107adantl 452 . . . . . . . . . . . . . . . . 17
109108, 17syldan 456 . . . . . . . . . . . . . . . 16
11080simplbi 446 . . . . . . . . . . . . . . . 16
111109, 110syl 15 . . . . . . . . . . . . . . 15
112111adantlr 695 . . . . . . . . . . . . . 14
113109, 81syl 15 . . . . . . . . . . . . . . 15
114113adantlr 695 . . . . . . . . . . . . . 14
115 simpr 447 . . . . . . . . . . . . . 14
116106, 112, 114, 115fsumless 12256 . . . . . . . . . . . . 13
117116ex 423 . . . . . . . . . . . 12
118117reximdv 2656 . . . . . . . . . . 11
119118imp 418 . . . . . . . . . 10
120104, 119sylan2 460 . . . . . . . . 9
121 breq1 4028 . . . . . . . . . 10
122121rexbidv 2566 . . . . . . . . 9
123120, 122syl5ibrcom 213 . . . . . . . 8
124123rexlimdva 2669 . . . . . . 7
125124imp 418 . . . . . 6
126103, 125sylan2b 461 . . . . 5
127 simpr 447 . . . . . . . . . . . 12
128 inss2 3392 . . . . . . . . . . . . . . 15
129 simpr 447 . . . . . . . . . . . . . . 15
130128, 129sseldi 3180 . . . . . . . . . . . . . 14
131 simpll 730 . . . . . . . . . . . . . . . 16
132 inss1 3391 . . . . . . . . . . . . . . . . . . 19
133 simplr 731 . . . . . . . . . . . . . . . . . . 19
134132, 133sseldi 3180 . . . . . . . . . . . . . . . . . 18
135 elpwi 3635 . . . . . . . . . . . . . . . . . 18
136134, 135syl 15 . . . . . . . . . . . . . . . . 17
137 simpr 447 . . . . . . . . . . . . . . . . 17
138136, 137sseldd 3183 . . . . . . . . . . . . . . . 16
139131, 138, 17syl2anc 642 . . . . . . . . . . . . . . 15
140139, 110syl 15 . . . . . . . . . . . . . 14
141130, 140fsumrecl 12209 . . . . . . . . . . . . 13
142141adantr 451 . . . . . . . . . . . 12
143127, 142eqeltrd 2359 . . . . . . . . . . 11
144143ex 423 . . . . . . . . . 10
145144rexlimdva 2669 . . . . . . . . 9
146145imp 418 . . . . . . . 8
147103, 146sylan2b 461 . . . . . . 7
148147adantr 451 . . . . . 6
149105, 111fsumrecl 12209 . . . . . . 7
150149ad2antrr 706 . . . . . 6
15199adantr 451 . . . . . . 7
152151adantr 451 . . . . . 6
153 simprr 733 . . . . . 6
154 frn 5397 . . . . . . . . 9
15525, 154syl 15 . . . . . . . 8
156155ad2antrr 706 . . . . . . 7
157 1nn 9759 . . . . . . . . . 10
158 ne0i 3463 . . . . . . . . . 10
159157, 158ax-mp 8 . . . . . . . . 9
160 dm0rn0 4897 . . . . . . . . . . 11
161 fdm 5395 . . . . . . . . . . . . 13
16225, 161syl 15 . . . . . . . . . . . 12
163 eqeq1 2291 . . . . . . . . . . . 12
164162, 163syl 15 . . . . . . . . . . 11
165160, 164syl5bbr 250 . . . . . . . . . 10
166165necon3bid 2483 . . . . . . . . 9
167159, 166mpbiri 224 . . . . . . . 8
168167ad2antrr 706 . . . . . . 7
169 seqfn 11060 . . . . . . . . . . . . . . . 16
1704, 169ax-mp 8 . . . . . . . . . . . . . . 15
1713fneq2i 5341 . . . . . . . . . . . . . . 15
172170, 171mpbir 200 . . . . . . . . . . . . . 14
173 dffn5 5570 . . . . . . . . . . . . . 14
174172, 173mpbi 199 . . . . . . . . . . . . 13
175 fvex 5541 . . . . . . . . . . . . 13
176174, 175elrnmpti 4932 . . . . . . . . . . . 12
177 r19.29 2685 . . . . . . . . . . . . 13
178 breq1 4028 . . . . . . . . . . . . . . 15
179178biimparc 473 . . . . . . . . . . . . . 14
180179rexlimivw 2665 . . . . . . . . . . . . 13
181177, 180syl 15 . . . . . . . . . . . 12
182176, 181sylan2b 461 . . . . . . . . . . 11
183182ralrimiva 2628 . . . . . . . . . 10
184183reximi 2652 . . . . . . . . 9
18590, 184syl 15 . . . . . . . 8
186185ad2antrr 706 . . . . . . 7
187 simpll 730 . . . . . . . 8
188 simpr 447 . . . . . . . . 9
189188ad2ant2r 727 . . . . . . . 8
190 simpll 730 . . . . . . . . . . . 12
191107adantl 452 . . . . . . . . . . . 12
192190, 191, 44syl2anc 642 . . . . . . . . . . 11
193188, 3syl6eleq 2375 . . . . . . . . . . 11
194190, 191, 17syl2anc 642 . . . . . . . . . . . . 13
195194, 110syl 15 . . . . . . . . . . . 12
196195recnd 8863 . . . . . . . . . . 11
197192, 193, 196fsumser 12205 . . . . . . . . . 10
198 fveq2 5527 . . . . . . . . . . . 12
199198eqeq2d 2296 . . . . . . . . . . 11
200199rspcev 2886 . . . . . . . . . 10
201188, 197, 200syl2anc 642 . . . . . . . . 9
202174, 175elrnmpti 4932 . . . . . . . . 9
203201, 202sylibr 203 . . . . . . . 8
204187, 189, 203syl2anc 642 . . . . . . 7
205 suprub 9717 . . . . . . 7
206156, 168, 186, 204, 205syl31anc 1185 . . . . . 6
207148, 150, 152, 153, 206letrd 8975 . . . . 5
208126, 207rexlimddv 2673 . . . 4
209147, 151lenltd 8967 . . . 4
210208, 209mpbid 201 . . 3
211 simpr1r 1013 . . . . . . 7
2122113anassrs 1173 . . . . . 6
213100ad3antrrr 710 . . . . . . . 8
214 pnfnlt 10469 . . . . . . . 8
215213, 214syl 15 . . . . . . 7
216 breq1 4028 . . . . . . . . 9
217216notbid 285 . . . . . . . 8
218217adantl 452 . . . . . . 7
219215, 218mpbird 223 . . . . . 6
220212, 219pm2.21dd 99 . . . . 5
221 simplll 734 . . . . . 6
222 simpr1l 1012 . . . . . . . 8
2232223anassrs 1173 . . . . . . 7
224 simplr 731 . . . . . . 7
225 simpr 447 . . . . . . 7
226 0xr 8880 . . . . . . . . 9
227 elico1 10701 . . . . . . . . 9
228226, 46, 227mp2an 653 . . . . . . . 8
229228biimpri 197 . . . . . . 7
230223, 224, 225, 229syl3anc 1182 . . . . . 6
231 simpr1r 1013 . . . . . . 7
2322313anassrs 1173 . . . . . 6
233155adantr 451 . . . . . . . . 9
234167adantr 451 . . . . . . . . 9
235185adantr 451 . . . . . . . . 9
236233, 234, 2353jca 1132 . . . . . . . 8
237 icossxr 10736 . . . . . . . . . 10
238 simprl 732 . . . . . . . . . 10
239237, 238sseldi 3180 . . . . . . . . 9
240 suprcl 9716 . . . . . . . . . 10
241236, 240syl 15 . . . . . . . . 9
242 elrege0 10748 . . . . . . . . . . 11
243242simprbi 450 . . . . . . . . . 10
244238, 243syl 15 . . . . . . . . 9
245100adantr 451 . . . . . . . . . 10
246 simprr 733 . . . . . . . . . 10
247 xrltle 10485 . . . . . . . . . . 11
248247imp 418 . . . . . . . . . 10
249239, 245, 246, 248syl21anc 1181 . . . . . . . . 9
250 xrrege0 10505 . . . . . . . . 9
251239, 241, 244, 249, 250syl22anc 1183 . . . . . . . 8
252 suprlub 9718 . . . . . . . . . 10
253252biimpd 198 . . . . . . . . 9
254253imp 418 . . . . . . . 8
255236, 251, 246, 254syl21anc 1181 . . . . . . 7
25660ssriv 3186 . . . . . . . . . . . . . . . . 17
257 ovex 5885 . . . . . . . . . . . . . . . . . 18
258257elpw 3633 . . . . . . . . . . . . . . . . 17
259256, 258mpbir 200 . . . . . . . . . . . . . . . 16
260 fzfi 11036 . . . . . . . . . . . . . . . 16
261 elin 3360 . . . . . . . . . . . . . . . 16
262259, 260, 261mpbir2an 886 . . . . . . . . . . . . . . 15
263262a1i 10 . . . . . . . . . . . . . 14
264 simpr 447 . . . . . . . . . . . . . . 15
26564adantr 451 . . . . . . . . . . . . . . 15
266264, 265eqtr4d 2320 . . . . . . . . . . . . . 14
267 sumeq1 12164 . . . . . . . . . . . . . . . 16
268267eqeq2d 2296 . . . . . . . . . . . . . . 15
269268rspcev 2886 . . . . . . . . . . . . . 14
270263, 266, 269syl2anc 642 . . . . . . . . . . . . 13
271270ex 423 . . . . . . . . . . . 12
272271rexlimdva 2669 . . . . . . . . . . 11
273174, 175elrnmpti 4932 . . . . . . . . . . . 12
274273a1i 10 . . . . . . . . . . 11
275101, 102elrnmpti 4932 . . . . . . . . . . . 12
276275a1i 10 . . . . . . . . . . 11
277272, 274, 2763imtr4d 259 . . . . . . . . . 10
278277ssrdv 3187 . . . . . . . . 9
279 ssrexv 3240 . . . . . . . . 9
280278, 279syl 15 . . . . . . . 8
281280imp 418 . . . . . . 7
282255, 281syldan 456 . . . . . 6
283221, 230, 232, 282syl12anc 1180 . . . . 5
284 simplrl 736 . . . . . 6
285 xrlelttric 23252 . . . . . . . 8
28646, 285mpan 651 . . . . . . 7
287 xgtpnf 23116 . . . . . . . 8
288287orbi1d 683 . . . . . . 7
289286, 288mpbid 201 . . . . . 6
290284, 289syl 15 . . . . 5
291220, 283, 290mpjaodan 761 . . . 4
292 0elpw 4182 . . . . . . . . 9
293 0fin 7089 . . . . . . . . 9
294 elin 3360 . . . . . . . . 9
295292, 293, 294mpbir2an 886 . . . . . . . 8
296 sum0 12196 . . . . . . . . 9
297296eqcomi 2289 . . . . . . . 8
298 sumeq1 12164 . . . . . . . . . 10
299298eqeq2d 2296 . . . . . . . . 9
300299rspcev 2886 . . . . . . . 8
301295, 297, 300mp2an 653 . . . . . . 7
302101, 102elrnmpti 4932 . . . . . . 7
303301, 302mpbir 200 . . . . . 6
304 breq2 4029 . . . . . . 7
305304rspcev 2886 . . . . . 6
306303, 305mpan 651 . . . . 5
307306adantl 452 . . . 4
308 xrlelttric 23252 . . . . . 6
309226, 308mpan 651 . . . . 5
310309ad2antrl 708 . . . 4
311291, 307, 310mpjaodan 761 . . 3
3122, 100, 210, 311eqsupd 7210 . 2
313 nfv 1607 . . 3
314 nfcv 2421 . . 3
315 nnex 9754 . . . 4
316315a1i 10 . . 3
317 icossicc 23260 . . . 4
318317, 17sseldi 3180 . . 3
319 elex 2798 . . . . . 6
320319adantl 452 . . . . 5
321 eqid 2285 . . . . . 6
322139, 321fmptd 5686 . . . . 5
323 esumpfinvallem 23444 . . . . 5 fld g s g
324320, 322, 323syl2anc 642 . . . 4 fld g s g
325140recnd 8863 . . . . 5
326130, 325gsumfsum 16441 . . . 4 fld g
327324, 326eqtr3d 2319 . . 3 s g
328313, 314, 316, 318, 327esumval 23427 . 2 Σ*
329 climuni 12028 . . 3
33070, 91, 329syl2anc 642 . 2
331312, 328, 3303eqtr4d 2327 1 Σ*
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 176   wo 357   wa 358   w3a 934   wceq 1625   wcel 1686   wne 2448  wral 2545  wrex 2546  cvv 2790   cin 3153   wss 3154  c0 3457  cpw 3627   class class class wbr 4025   cmpt 4079   wor 4315   cdm 4691   crn 4692   wfn 5252  wf 5253  cfv 5257  (class class class)co 5860  cfn 6865  csup 7195  cc 8737  cr 8738  cc0 8739  c1 8740   caddc 8742   cpnf 8866   cmnf 8867  cxr 8868   clt 8869   cle 8870  cn 9748  cz 10026  cuz 10232  cioo 10658  cico 10660  cicc 10661  cfz 10784   cseq 11048   cli 11960  csu 12160   ↾s cress 13151  cxrs 13401   g cgsu 13403  ℂfldccnfld 16379  Σ*cesum 23412 This theorem is referenced by:  esumcvg  23456 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-13 1688  ax-14 1690  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266  ax-rep 4133  ax-sep 4143  ax-nul 4151  ax-pow 4190  ax-pr 4216  ax-un 4514  ax-inf2 7344  ax-cnex 8795  ax-resscn 8796  ax-1cn 8797  ax-icn 8798  ax-addcl 8799  ax-addrcl 8800  ax-mulcl 8801  ax-mulrcl 8802  ax-mulcom 8803  ax-addass 8804  ax-mulass 8805  ax-distr 8806  ax-i2m1 8807  ax-1ne0 8808  ax-1rid 8809  ax-rnegex 8810  ax-rrecex 8811  ax-cnre 8812  ax-pre-lttri 8813  ax-pre-lttrn 8814  ax-pre-ltadd 8815  ax-pre-mulgt0 8816  ax-pre-sup 8817  ax-addf 8818  ax-mulf 8819 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-eu 2149  df-mo 2150  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-nel 2451  df-ral 2550  df-rex 2551  df-reu 2552  df-rmo 2553  df-rab 2554  df-v 2792  df-sbc 2994  df-csb 3084  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-pss 3170  df-nul 3458  df-if 3568  df-pw 3629  df-sn 3648  df-pr 3649  df-tp 3650  df-op 3651  df-uni 3830  df-int 3865  df-iun 3909  df-iin 3910  df-br 4026  df-opab 4080  df-mpt 4081  df-tr 4116  df-eprel 4307  df-id 4311  df-po 4316  df-so 4317  df-fr 4354  df-se 4355  df-we 4356  df-ord 4397  df-on 4398  df-lim 4399  df-suc 4400  df-om 4659  df-xp 4697  df-rel 4698  df-cnv 4699  df-co 4700  df-dm 4701  df-rn 4702  df-res 4703  df-ima 4704  df-iota 5221  df-fun 5259  df-fn 5260  df-f 5261  df-f1 5262  df-fo 5263  df-f1o 5264  df-fv 5265  df-isom 5266  df-ov 5863  df-oprab 5864  df-mpt2 5865  df-of 6080  df-1st 6124  df-2nd 6125  df-riota 6306  df-recs 6390  df-rdg 6425  df-1o 6481  df-oadd 6485  df-er 6662  df-map 6776  df-pm 6777  df-en 6866  df-dom 6867  df-sdom 6868  df-fin 6869  df-fi 7167  df-sup 7196  df-oi 7227  df-card 7574  df-pnf 8871  df-mnf 8872  df-xr 8873  df-ltxr 8874  df-le 8875  df-sub 9041  df-neg 9042  df-div 9426  df-nn 9749  df-2 9806  df-3 9807  df-4 9808  df-5 9809  df-6 9810  df-7 9811  df-8 9812  df-9 9813  df-10 9814  df-n0 9968  df-z 10027  df-dec 10127  df-uz 10233  df-q 10319  df-rp 10357  df-xadd 10455  df-ioo 10662  df-ioc 10663  df-ico 10664  df-icc 10665  df-fz 10785  df-fzo 10873  df-fl 10927  df-seq 11049  df-exp 11107  df-hash 11340  df-cj 11586  df-re 11587  df-im 11588  df-sqr 11722  df-abs 11723  df-clim 11964  df-rlim 11965  df-sum 12161  df-struct 13152  df-ndx 13153  df-slot 13154  df-base 13155  df-sets 13156  df-ress 13157  df-plusg 13223  df-mulr 13224  df-starv 13225  df-tset 13229  df-ple 13230  df-ds 13232  df-rest 13329  df-topn 13330  df-topgen 13346  df-ordt 13404  df-xrs 13405  df-0g 13406  df-gsum 13407  df-mre 13490  df-mrc 13491  df-acs 13493  df-ps 14308  df-tsr 14309  df-mnd 14369  df-submnd 14418  df-grp 14491  df-minusg 14492  df-cntz 14795  df-cmn 15093  df-abl 15094  df-mgp 15328  df-rng 15342  df-cring 15343  df-ur 15344  df-cnfld 16380  df-top 16638  df-bases 16640  df-topon 16641  df-topsp 16642  df-ntr 16759  df-nei 16837  df-cn 16959  df-haus 17045  df-fbas 17522  df-fg 17523  df-fil 17543  df-fm 17635  df-flim 17636  df-flf 17637  df-tsms 17811  df-esum 23413
 Copyright terms: Public domain W3C validator