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

Theorem fisumcvg2 10786
 Description: The sequence of partial sums of a finite sum converges to the whole sum. (Contributed by Mario Carneiro, 20-Apr-2014.) Use fsum3cvg2 10787 instead. (New usage is discouraged.)
Hypotheses
Ref Expression
fsumsers.1
fsumsers.2
fsumsers.3
fsumsers.dc DECID
fsumsers.4
Assertion
Ref Expression
fisumcvg2
Distinct variable groups:   ,   ,   ,   ,   ,
Allowed substitution hint:   ()

Proof of Theorem fisumcvg2
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nfcv 2228 . . . 4
2 nfv 1466 . . . . 5
3 nfcsb1v 2963 . . . . 5
4 nfcv 2228 . . . . 5
52, 3, 4nfif 3419 . . . 4
6 eleq1w 2148 . . . . 5
7 csbeq1a 2941 . . . . 5
86, 7ifbieq1d 3413 . . . 4
91, 5, 8cbvmpt 3933 . . 3
10 fsumsers.3 . . . . 5
1110ralrimiva 2446 . . . 4
123nfel1 2239 . . . . 5
137eleq1d 2156 . . . . 5
1412, 13rspc 2716 . . . 4
1511, 14mpan9 275 . . 3
166dcbid 786 . . . 4 DECID DECID
17 fsumsers.dc . . . . . 6 DECID
1817ralrimiva 2446 . . . . 5 DECID
1918adantr 270 . . . 4 DECID
20 simpr 108 . . . 4
2116, 19, 20rspcdva 2727 . . 3 DECID
22 fsumsers.2 . . 3
23 fsumsers.4 . . 3
249, 15, 21, 22, 23fisumcvg 10766 . 2
25 eluzel2 9024 . . . 4
2622, 25syl 14 . . 3
27 fveq2 5305 . . . . 5
2827eleq1d 2156 . . . 4
29 fsumsers.1 . . . . . . 7
3010adantlr 461 . . . . . . . 8
31 0cnd 7481 . . . . . . . 8
3230, 31, 17ifcldadc 3420 . . . . . . 7
3329, 32eqeltrd 2164 . . . . . 6
3433ralrimiva 2446 . . . . 5
3534adantr 270 . . . 4
36 simpr 108 . . . 4
3728, 35, 36rspcdva 2727 . . 3
38 eluzelz 9028 . . . . . . 7
39 eqid 2088 . . . . . . . 8
4039fvmpt2 5386 . . . . . . 7
4138, 32, 40syl2an2 561 . . . . . 6
4229, 41eqtr4d 2123 . . . . 5
4342ralrimiva 2446 . . . 4
44 nffvmpt1 5316 . . . . . 6
4544nfeq2 2240 . . . . 5
46 fveq2 5305 . . . . . 6
47 fveq2 5305 . . . . . 6
4846, 47eqeq12d 2102 . . . . 5
4945, 48rspc 2716 . . . 4
5043, 49mpan9 275 . . 3
51 addcl 7467 . . . 4