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	|- ( ph -> N e. NN0 )
	fz1sumconst.c	|- ( ph -> C e. CC )
Assertion	fz1sumconst	|- ( ph -> sum_ k e. ( 1 ... N ) C = ( N x. C ) )

Proof

Step	Hyp	Ref	Expression
1		fz1sumconst.n	|- ( ph -> N e. NN0 )
2		fz1sumconst.c	|- ( ph -> C e. CC )
3		fzfi	|- ( 1 ... N ) e. Fin
4		fsumconst	|- ( ( ( 1 ... N ) e. Fin /\ C e. CC ) -> sum_ k e. ( 1 ... N ) C = ( ( # ` ( 1 ... N ) ) x. C ) )
5	3 2 4	sylancr	|- ( ph -> sum_ k e. ( 1 ... N ) C = ( ( # ` ( 1 ... N ) ) x. C ) )
6		hashfz1	|- ( N e. NN0 -> ( # ` ( 1 ... N ) ) = N )
7	1 6	syl	|- ( ph -> ( # ` ( 1 ... N ) ) = N )
8	7	oveq1d	|- ( ph -> ( ( # ` ( 1 ... N ) ) x. C ) = ( N x. C ) )
9	5 8	eqtrd	|- ( ph -> sum_ k e. ( 1 ... N ) C = ( N x. C ) )