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 -> A = B )
Assertion	fsum1	|- ( ( M e. ZZ /\ B e. CC ) -> sum_ k e. ( M ... M ) A = B )

Proof

Step	Hyp	Ref	Expression
1		fsum1.1	|- ( k = M -> A = B )
2		fzsn	|- ( M e. ZZ -> ( M ... M ) = { M } )
3	2	adantr	|- ( ( M e. ZZ /\ B e. CC ) -> ( M ... M ) = { M } )
4	3	sumeq1d	|- ( ( M e. ZZ /\ B e. CC ) -> sum_ k e. ( M ... M ) A = sum_ k e. { M } A )
5	1	sumsn	|- ( ( M e. ZZ /\ B e. CC ) -> sum_ k e. { M } A = B )
6	4 5	eqtrd	|- ( ( M e. ZZ /\ B e. CC ) -> sum_ k e. ( M ... M ) A = B )