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

Theorem fsumconst 13844
 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 9813 . . . . 5
21adantl 468 . . . 4
32eqcomd 2431 . . 3
4 sumeq1 13748 . . . . 5
5 sum0 13780 . . . . 5
64, 5syl6eq 2480 . . . 4
7 fveq2 5879 . . . . . 6
8 hash0 12549 . . . . . 6
97, 8syl6eq 2480 . . . . 5
109oveq1d 6318 . . . 4
116, 10eqeq12d 2445 . . 3
123, 11syl5ibrcom 226 . 2
13 eqidd 2424 . . . . . . 7
14 simprl 763 . . . . . . 7
15 simprr 765 . . . . . . 7
16 simpllr 768 . . . . . . 7
17 simplr 761 . . . . . . . 8
18 elfznn 11830 . . . . . . . 8
19 fvconst2g 6131 . . . . . . . 8
2017, 18, 19syl2an 480 . . . . . . 7
2113, 14, 15, 16, 20fsum 13779 . . . . . 6
22 ser1const 12270 . . . . . . 7
2322ad2ant2lr 753 . . . . . 6
2421, 23eqtrd 2464 . . . . 5
2524expr 619 . . . 4
2625exlimdv 1769 . . 3
2726expimpd 607 . 2
28 fz1f1o 13769 . . 3