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

Metamath Proof Explorer

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	$⊢ (M \in ℤ \land B \in ℂ) \to \sum_{k = M}^{M} A = B$

Proof

Step	Hyp	Ref	Expression
1		fsum1.1	$⊢ k = M \to A = B$
2		fzsn	$⊢ M \in ℤ \to (M \dots M) = \{M\}$
3	2	adantr	$⊢ (M \in ℤ \land B \in ℂ) \to (M \dots M) = \{M\}$
4	3	sumeq1d	$⊢ (M \in ℤ \land B \in ℂ) \to \sum_{k = M}^{M} A = \sum_{k \in \{M\}} A$
5	1	sumsn	$⊢ (M \in ℤ \land B \in ℂ) \to \sum_{k \in \{M\}} A = B$
6	4 5	eqtrd	$⊢ (M \in ℤ \land B \in ℂ) \to \sum_{k = M}^{M} A = B$