This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∈ Fin → ∑ k ∈ A 1 = A

Proof

Step Hyp Ref Expression
1 1cnd ⊢ A ∈ Fin → 1 ∈ ℂ
2 fsumconst ⊢ A ∈ Fin ∧ 1 ∈ ℂ → ∑ k ∈ A 1 = A ⋅ 1
3 1 2 mpdan ⊢ A ∈ Fin → ∑ k ∈ A 1 = A ⋅ 1
4 hashcl ⊢ A ∈ Fin → A ∈ ℕ 0
5 4 nn0cnd ⊢ A ∈ Fin → A ∈ ℂ
6 5 mulridd ⊢ A ∈ Fin → A ⋅ 1 = A
7 3 6 eqtrd ⊢ A ∈ Fin → ∑ k ∈ A 1 = A