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

Theorem fsumconst 12561
 Description: The sum of constant terms ( is not free in ). (Contributed by NM, 24-Dec-2005.) (Revised by Mario Carneiro, 24-Apr-2014.)
Assertion
Ref Expression
fsumconst
Distinct variable groups:   ,   ,

Proof of Theorem fsumconst
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mul02 9233 . . . . 5
21adantl 453 . . . 4
32eqcomd 2440 . . 3
4 sumeq1 12471 . . . . 5
5 sum0 12503 . . . . 5
64, 5syl6eq 2483 . . . 4
7 fveq2 5719 . . . . . 6
8 hash0 11634 . . . . . 6
97, 8syl6eq 2483 . . . . 5
109oveq1d 6087 . . . 4
116, 10eqeq12d 2449 . . 3
123, 11syl5ibrcom 214 . 2
13 eqidd 2436 . . . . . . 7
14 simprl 733 . . . . . . 7
15 simprr 734 . . . . . . 7
16 simpllr 736 . . . . . . 7
17 simplr 732 . . . . . . . 8
18 elfznn 11069 . . . . . . . 8
19 fvconst2g 5936 . . . . . . . 8
2017, 18, 19syl2an 464 . . . . . . 7
2113, 14, 15, 16, 20fsum 12502 . . . . . 6
22 ser1const 11367 . . . . . . 7
2322ad2ant2lr 729 . . . . . 6
2421, 23eqtrd 2467 . . . . 5
2524expr 599 . . . 4
2625exlimdv 1646 . . 3
2726expimpd 587 . 2
28 fz1f1o 12492 . . 3