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	⊢ ( 𝐴 ∈ Fin → Σ 𝑘 ∈ 𝐴 1 = ( ♯ ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		1cnd	⊢ ( 𝐴 ∈ Fin → 1 ∈ ℂ )
2		fsumconst	⊢ ( ( 𝐴 ∈ Fin ∧ 1 ∈ ℂ ) → Σ 𝑘 ∈ 𝐴 1 = ( ( ♯ ‘ 𝐴 ) · 1 ) )
3	1 2	mpdan	⊢ ( 𝐴 ∈ Fin → Σ 𝑘 ∈ 𝐴 1 = ( ( ♯ ‘ 𝐴 ) · 1 ) )
4		hashcl	⊢ ( 𝐴 ∈ Fin → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
5	4	nn0cnd	⊢ ( 𝐴 ∈ Fin → ( ♯ ‘ 𝐴 ) ∈ ℂ )
6	5	mulridd	⊢ ( 𝐴 ∈ Fin → ( ( ♯ ‘ 𝐴 ) · 1 ) = ( ♯ ‘ 𝐴 ) )
7	3 6	eqtrd	⊢ ( 𝐴 ∈ Fin → Σ 𝑘 ∈ 𝐴 1 = ( ♯ ‘ 𝐴 ) )