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

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

Proof of Theorem fsum3ser
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2115 . . . . 5
2 eleq1w 2176 . . . . . 6
3 fveq2 5387 . . . . . 6
42, 3ifbieq1d 3462 . . . . 5
5 simpr 109 . . . . 5
6 fsum3ser.1 . . . . . . . 8
7 fsum3ser.3 . . . . . . . 8
86, 7eqeltrd 2192 . . . . . . 7
98adantr 272 . . . . . 6
10 0cnd 7723 . . . . . 6
11 eluzelz 9287 . . . . . . 7
12 eluzel2 9283 . . . . . . 7
13 fsum3ser.2 . . . . . . . . 9
14 eluzelz 9287 . . . . . . . . 9
1513, 14syl 14 . . . . . . . 8
1615adantr 272 . . . . . . 7
17 fzdcel 9771 . . . . . . 7 DECID
1811, 12, 16, 17syl2an23an 1260 . . . . . 6 DECID
199, 10, 18ifcldadc 3469 . . . . 5
201, 4, 5, 19fvmptd3 5480 . . . 4
216ifeq1d 3457 . . . 4
2220, 21eqtrd 2148 . . 3
23 elfzuz 9753 . . . 4
2423, 7sylan2 282 . . 3
25 ssidd 3086 . . 3
2622, 13, 24, 18, 25fsumsersdc 11115 . 2
2723, 20sylan2 282 . . . 4
28 iftrue 3447 . . . . 5
2928adantl 273 . . . 4
3027, 29eqtrd 2148 . . 3
31 eleq1w 2176 . . . . . 6
32 fveq2 5387 . . . . . 6
3331, 32ifbieq1d 3462 . . . . 5
34 simpr 109 . . . . 5
35 fveq2 5387 . . . . . . . 8
3635eleq1d 2184 . . . . . . 7
378ralrimiva 2480 . . . . . . . 8
3837adantr 272 . . . . . . 7
3936, 38, 34rspcdva 2766 . . . . . 6
40 0cnd 7723 . . . . . 6
41 eluzelz 9287 . . . . . . 7
42 eluzel2 9283 . . . . . . 7
4315adantr 272 . . . . . . 7
44 fzdcel 9771 . . . . . . 7 DECID
4541, 42, 43, 44syl2an23an 1260 . . . . . 6 DECID
4639, 40, 45ifcldcd 3475 . . . . 5
471, 33, 34, 46fvmptd3 5480 . . . 4
4847, 46eqeltrd 2192 . . 3
4936cbvralv 2629 . . . . 5
5037, 49sylib 121 . . . 4
5150r19.21bi 2495 . . 3
52 addcl 7709 . . . 4