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

Metamath Proof Explorer

Theorem sumsns

Description: A sum of a singleton is the term. (Contributed by Mario Carneiro, 22-Apr-2014)

Ref Expression
Assertion sumsns ⊢ M ∈ V ∧ ⦋ M / k⦌ A ∈ ℂ → ∑ k ∈ M A = ⦋ M / k⦌ A

Proof

Step Hyp Ref Expression
1 csbeq1a ⊢ k = n → A = ⦋ n / k⦌ A
2 nfcv ⊢ Ⅎ _ n A
3 nfcsb1v ⊢ Ⅎ _ k ⦋ n / k⦌ A
4 1 2 3 cbvsum ⊢ ∑ k ∈ M A = ∑ n ∈ M ⦋ n / k⦌ A
5 csbeq1 ⊢ n = M → ⦋ n / k⦌ A = ⦋ M / k⦌ A
6 5 sumsn ⊢ M ∈ V ∧ ⦋ M / k⦌ A ∈ ℂ → ∑ n ∈ M ⦋ n / k⦌ A = ⦋ M / k⦌ A
7 4 6 eqtrid ⊢ M ∈ V ∧ ⦋ M / k⦌ A ∈ ℂ → ∑ k ∈ M A = ⦋ M / k⦌ A