Description: The sum of N constant terms ( k is not free in C ). (Contributed by SN, 21-Mar-2025)
Ref | Expression | ||
---|---|---|---|
Hypotheses | fz1sumconst.n | ||
fz1sumconst.c | |||
Assertion | fz1sumconst |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fz1sumconst.n | ||
2 | fz1sumconst.c | ||
3 | fzfi | ||
4 | fsumconst | ||
5 | 3 2 4 | sylancr | |
6 | hashfz1 | ||
7 | 1 6 | syl | |
8 | 7 | oveq1d | |
9 | 5 8 | eqtrd |