Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  fsum3cvg2 Unicode version

Theorem fsum3cvg2 11170
 Description: The sequence of partial sums of a finite sum converges to the whole sum. (Contributed by Mario Carneiro, 20-Apr-2014.) (Revised by Jim Kingdon, 2-Dec-2022.)
Hypotheses
Ref Expression
fsumsers.1
fsumsers.2
fsumsers.3
fsumsers.dc DECID
fsumsers.4
Assertion
Ref Expression
fsum3cvg2
Distinct variable groups:   ,   ,   ,   ,   ,
Allowed substitution hint:   ()

Proof of Theorem fsum3cvg2
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nfcv 2281 . . . 4
2 nfv 1508 . . . . 5
3 nfcsb1v 3035 . . . . 5
4 nfcv 2281 . . . . 5
52, 3, 4nfif 3500 . . . 4
6 eleq1w 2200 . . . . 5
7 csbeq1a 3012 . . . . 5
86, 7ifbieq1d 3494 . . . 4
91, 5, 8cbvmpt 4023 . . 3
10 fsumsers.3 . . . . 5
1110ralrimiva 2505 . . . 4
123nfel1 2292 . . . . 5
137eleq1d 2208 . . . . 5
1412, 13rspc 2783 . . . 4
1511, 14mpan9 279 . . 3
166dcbid 823 . . . 4 DECID DECID
17 fsumsers.dc . . . . . 6 DECID
1817ralrimiva 2505 . . . . 5 DECID
1918adantr 274 . . . 4 DECID
20 simpr 109 . . . 4
2116, 19, 20rspcdva 2794 . . 3 DECID
22 fsumsers.2 . . 3
23 fsumsers.4 . . 3
249, 15, 21, 22, 23fsum3cvg 11154 . 2
25 eluzel2 9338 . . . 4
2622, 25syl 14 . . 3
27 fveq2 5421 . . . . 5
2827eleq1d 2208 . . . 4
29 fsumsers.1 . . . . . . 7
3010adantlr 468 . . . . . . . 8
31 0cnd 7766 . . . . . . . 8
3230, 31, 17ifcldadc 3501 . . . . . . 7
3329, 32eqeltrd 2216 . . . . . 6
3433ralrimiva 2505 . . . . 5
3534adantr 274 . . . 4
36 simpr 109 . . . 4
3728, 35, 36rspcdva 2794 . . 3
38 eluzelz 9342 . . . . . . 7
39 eqid 2139 . . . . . . . 8
4039fvmpt2 5504 . . . . . . 7
4138, 32, 40syl2an2 583 . . . . . 6
4229, 41eqtr4d 2175 . . . . 5
4342ralrimiva 2505 . . . 4
44 nffvmpt1 5432 . . . . . 6
4544nfeq2 2293 . . . . 5
46 fveq2 5421 . . . . . 6
47 fveq2 5421 . . . . . 6
4846, 47eqeq12d 2154 . . . . 5
4945, 48rspc 2783 . . . 4
5043, 49mpan9 279 . . 3
51 addcl 7752 . . . 4