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	$$⊢\phi \to N\in {\mathbb{N}}_0$$
	fz1sumconst.c	$$⊢\phi \to C\in ℂ$$
Assertion	fz1sumconst	$$⊢\phi \to \sum _{k=1}^{N}C=NC$$

Proof

Step	Hyp	Ref	Expression
1		fz1sumconst.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
2		fz1sumconst.c	$$⊢\phi \to C\in ℂ$$
3		fzfi	$$⊢\left(1\dots N\right)\in \mathrm{Fin}$$
4		fsumconst	$$⊢\left(\left(1\dots N\right)\in \mathrm{Fin}\wedge C\in ℂ\right)\to \sum _{k=1}^{N}C=\left|\left(1\dots N\right)\right|C$$
5	3 2 4	sylancr	$$⊢\phi \to \sum _{k=1}^{N}C=\left|\left(1\dots N\right)\right|C$$
6		hashfz1	$$⊢N\in {\mathbb{N}}_0\to \left|\left(1\dots N\right)\right|=N$$
7	1 6	syl	$$⊢\phi \to \left|\left(1\dots N\right)\right|=N$$
8	7	oveq1d	$$⊢\phi \to \left|\left(1\dots N\right)\right|C=NC$$
9	5 8	eqtrd	$$⊢\phi \to \sum _{k=1}^{N}C=NC$$