Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  fsumser Structured version   Unicode version

Theorem fsumser 12524
 Description: A finite sum expressed in terms of a partial sum of an infinite series. The recursive definition of follows as fsum1 12535 and fsump1i 12553, which should make our notation clear and from which, along with closure fsumcl 12527, we will derive the basic properties of finite sums. (Contributed by NM, 11-Dec-2005.) (Revised by Mario Carneiro, 21-Apr-2014.)
Hypotheses
Ref Expression
fsumser.1
fsumser.2
fsumser.3
Assertion
Ref Expression
fsumser
Distinct variable groups:   ,   ,   ,   ,
Allowed substitution hint:   ()

Proof of Theorem fsumser
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 eleq1 2496 . . . . . 6
2 fveq2 5728 . . . . . 6
3 eqidd 2437 . . . . . 6
41, 2, 3ifbieq12d 3761 . . . . 5
5 eqid 2436 . . . . 5
6 fvex 5742 . . . . . 6
7 c0ex 9085 . . . . . 6
86, 7ifex 3797 . . . . 5
94, 5, 8fvmpt 5806 . . . 4
10 fsumser.1 . . . . 5
1110ifeq1da 3764 . . . 4
129, 11sylan9eqr 2490 . . 3
13 fsumser.2 . . 3
14 fsumser.3 . . 3
15 ssid 3367 . . . 4
1615a1i 11 . . 3
1712, 13, 14, 16fsumsers 12522 . 2
18 elfzuz 11055 . . . . . 6
1918, 9syl 16 . . . . 5
20 iftrue 3745 . . . . 5
2119, 20eqtrd 2468 . . . 4