Theorem sumsns

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

	Ref	Expression
Assertion	sumsns	$$⊢\left(M\in V\wedge ⦋M/k⦌A\in ℂ\right)\to \sum _{k\in \left\{M\right\}}A=⦋M/k⦌A$$

Proof

Step	Hyp	Ref	Expression
1		nfcv	$$⊢\underset{\_}{Ⅎ}nA$$
2		nfcsb1v	$$⊢\underset{\_}{Ⅎ}k⦋n/k⦌A$$
3		csbeq1a	$$⊢k=n\to A=⦋n/k⦌A$$
4	1 2 3	cbvsumi	$$⊢\sum _{k\in \left\{M\right\}}A=\sum _{n\in \left\{M\right\}}⦋n/k⦌A$$
5		csbeq1	$$⊢n=M\to ⦋n/k⦌A=⦋M/k⦌A$$
6	5	sumsn	$$⊢\left(M\in V\wedge ⦋M/k⦌A\in ℂ\right)\to \sum _{n\in \left\{M\right\}}⦋n/k⦌A=⦋M/k⦌A$$
7	4 6	eqtrid	$$⊢\left(M\in V\wedge ⦋M/k⦌A\in ℂ\right)\to \sum _{k\in \left\{M\right\}}A=⦋M/k⦌A$$