Theorem fsumconst1

Description: The sum of 1 over a finite set equals the size of the set. (Contributed by AV, 10-Apr-2026)

	Ref	Expression
Assertion	fsumconst1	$$⊢A\in \mathrm{Fin}\to \sum _{k\in A}1=\left|A\right|$$

Proof

Step	Hyp	Ref	Expression
1		1cnd	$$⊢A\in \mathrm{Fin}\to 1\in ℂ$$
2		fsumconst	$$⊢\left(A\in \mathrm{Fin}\wedge 1\in ℂ\right)\to \sum _{k\in A}1=\left|A\right|\cdot 1$$
3	1 2	mpdan	$$⊢A\in \mathrm{Fin}\to \sum _{k\in A}1=\left|A\right|\cdot 1$$
4		hashcl	$$⊢A\in \mathrm{Fin}\to \left|A\right|\in {\mathbb{N}}_0$$
5	4	nn0cnd	$$⊢A\in \mathrm{Fin}\to \left|A\right|\in ℂ$$
6	5	mulridd	$$⊢A\in \mathrm{Fin}\to \left|A\right|\cdot 1=\left|A\right|$$
7	3 6	eqtrd	$$⊢A\in \mathrm{Fin}\to \sum _{k\in A}1=\left|A\right|$$