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 ( ( 𝑀𝑉 𝑀 / 𝑘 𝐴 ∈ ℂ ) → Σ 𝑘 ∈ { 𝑀 } 𝐴 = 𝑀 / 𝑘 𝐴 )

Proof

Step Hyp Ref Expression
1 nfcv 𝑛 𝐴
2 nfcsb1v 𝑘 𝑛 / 𝑘 𝐴
3 csbeq1a ( 𝑘 = 𝑛𝐴 = 𝑛 / 𝑘 𝐴 )
4 1 2 3 cbvsumi Σ 𝑘 ∈ { 𝑀 } 𝐴 = Σ 𝑛 ∈ { 𝑀 } 𝑛 / 𝑘 𝐴
5 csbeq1 ( 𝑛 = 𝑀 𝑛 / 𝑘 𝐴 = 𝑀 / 𝑘 𝐴 )
6 5 sumsn ( ( 𝑀𝑉 𝑀 / 𝑘 𝐴 ∈ ℂ ) → Σ 𝑛 ∈ { 𝑀 } 𝑛 / 𝑘 𝐴 = 𝑀 / 𝑘 𝐴 )
7 4 6 eqtrid ( ( 𝑀𝑉 𝑀 / 𝑘 𝐴 ∈ ℂ ) → Σ 𝑘 ∈ { 𝑀 } 𝐴 = 𝑀 / 𝑘 𝐴 )