Theorem fsum1

Description: The finite sum of A ( k ) from k = M to M (i.e. a sum with only one term) is B i.e. A ( M ) . (Contributed by NM, 8-Nov-2005) (Revised by Mario Carneiro, 21-Apr-2014)

	Ref	Expression
Hypothesis	fsum1.1	$$⊢k=M\to A=B$$
Assertion	fsum1	$$⊢\left(M\in \mathbb{Z}\wedge B\in ℂ\right)\to \sum _{k=M}^{M}A=B$$

Proof

Step	Hyp	Ref	Expression
1		fsum1.1	$$⊢k=M\to A=B$$
2		fzsn	$$⊢M\in \mathbb{Z}\to \left(M\dots M\right)=\left\{M\right\}$$
3	2	adantr	$$⊢\left(M\in \mathbb{Z}\wedge B\in ℂ\right)\to \left(M\dots M\right)=\left\{M\right\}$$
4	3	sumeq1d	$$⊢\left(M\in \mathbb{Z}\wedge B\in ℂ\right)\to \sum _{k=M}^{M}A=\sum _{k\in \left\{M\right\}}A$$
5	1	sumsn	$$⊢\left(M\in \mathbb{Z}\wedge B\in ℂ\right)\to \sum _{k\in \left\{M\right\}}A=B$$
6	4 5	eqtrd	$$⊢\left(M\in \mathbb{Z}\wedge B\in ℂ\right)\to \sum _{k=M}^{M}A=B$$