Metamath Proof Explorer


Theorem fz1sumconst

Description: The sum of N constant terms ( k is not free in C ). (Contributed by SN, 21-Mar-2025)

Ref Expression
Hypotheses fz1sumconst.n φ N 0
fz1sumconst.c φ C
Assertion fz1sumconst φ k = 1 N C = N C

Proof

Step Hyp Ref Expression
1 fz1sumconst.n φ N 0
2 fz1sumconst.c φ C
3 fzfi 1 N Fin
4 fsumconst 1 N Fin C k = 1 N C = 1 N C
5 3 2 4 sylancr φ k = 1 N C = 1 N C
6 hashfz1 N 0 1 N = N
7 1 6 syl φ 1 N = N
8 7 oveq1d φ 1 N C = N C
9 5 8 eqtrd φ k = 1 N C = N C