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

Theorem fisumser 10790
 Description: A finite sum expressed in terms of a partial sum of an infinite series. The recursive definition follows as fsum1 10806 and fsump1 10814, which should make our notation clear and from which, along with closure fsumcl 10794, we will derive the basic properties of finite sums. (Contributed by NM, 11-Dec-2005.) (Revised by Jim Kingdon, 1-Oct-2022.) Use fsum3ser 10791 instead. (New usage is discouraged.)
Hypotheses
Ref Expression
fisumser.1
fsumser.2
fisumser.3
Assertion
Ref Expression
fisumser
Distinct variable groups:   ,   ,   ,   ,
Allowed substitution hint:   ()

Proof of Theorem fisumser
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpr 108 . . . . 5
2 fisumser.1 . . . . . . . 8
3 fisumser.3 . . . . . . . 8
42, 3eqeltrd 2164 . . . . . . 7
54adantr 270 . . . . . 6
6 0cnd 7481 . . . . . 6
7 eluzelz 9028 . . . . . . 7
8 eluzel2 9024 . . . . . . 7
9 fsumser.2 . . . . . . . . 9
10 eluzelz 9028 . . . . . . . . 9
119, 10syl 14 . . . . . . . 8
1211adantr 270 . . . . . . 7
13 fzdcel 9454 . . . . . . 7 DECID
147, 8, 12, 13syl2an23an 1235 . . . . . 6 DECID
155, 6, 14ifcldadc 3420 . . . . 5
16 eleq1w 2148 . . . . . . 7
17 fveq2 5305 . . . . . . 7
1816, 17ifbieq1d 3413 . . . . . 6
19 eqid 2088 . . . . . 6
2018, 19fvmptg 5380 . . . . 5
211, 15, 20syl2anc 403 . . . 4
222ifeq1d 3408 . . . 4
2321, 22eqtrd 2120 . . 3
24 elfzuz 9436 . . . 4
2524, 3sylan2 280 . . 3
26 ssidd 3045 . . 3
2723, 9, 25, 14, 26fisumsers 10788 . 2
2824, 21sylan2 280 . . . 4
29 iftrue 3398 . . . . 5
3029adantl 271 . . . 4
3128, 30eqtrd 2120 . . 3
32 simpr 108 . . . . 5
33 fveq2 5305 . . . . . . . 8
3433eleq1d 2156 . . . . . . 7
354ralrimiva 2446 . . . . . . . 8
3635adantr 270 . . . . . . 7
3734, 36, 32rspcdva 2727 . . . . . 6
38 0cnd 7481 . . . . . 6
39 eluzelz 9028 . . . . . . 7
40 eluzel2 9024 . . . . . . 7
4111adantr 270 . . . . . . 7
42 fzdcel 9454 . . . . . . 7 DECID
4339, 40, 41, 42syl2an23an 1235 . . . . . 6 DECID
4437, 38, 43ifcldcd 3426 . . . . 5
45 eleq1w 2148 . . . . . . 7
46 fveq2 5305 . . . . . . 7
4745, 46ifbieq1d 3413 . . . . . 6
4847, 19fvmptg 5380 . . . . 5
4932, 44, 48syl2anc 403 . . . 4
5049, 44eqeltrd 2164 . . 3
5134cbvralv 2590 . . . . 5
5235, 51sylib 120 . . . 4
5352r19.21bi 2461 . . 3
54 addcl 7467 . . . 4