fzosump1

Description: Separate out the last term in a finite sum. (Contributed by Mario Carneiro, 13-Apr-2016)

Step	Hyp	Ref	Expression
1		fsumm1.1	$⊢ φ \to N \in ℤ_{\geq M}$
2		fsumm1.2	$⊢ (φ \land k \in (M \dots N)) \to A \in ℂ$
3		fsumm1.3	$⊢ k = N \to A = B$
4		eluzelz	$⊢ N \in ℤ_{\geq M} \to N \in ℤ$
5	1 4	syl	$⊢ φ \to N \in ℤ$
6		fzoval	$⊢ N \in ℤ \to (M ..^N) = (M \dots N - 1)$
7	5 6	syl	$⊢ φ \to (M ..^N) = (M \dots N - 1)$
8	7	sumeq1d	$⊢ φ \to \sum_{k \in (M ..^N)} A = \sum_{k = M}^{N - 1} A$
9	8	oveq1d	$⊢ φ \to \sum_{k \in (M ..^N)} A + B = \sum_{k = M}^{N - 1} A + B$
10	1 2 3	fsumm1	$⊢ φ \to \sum_{k = M}^{N} A = \sum_{k = M}^{N - 1} A + B$
11		fzval3	$⊢ N \in ℤ \to (M \dots N) = (M ..^N + 1)$
12	5 11	syl	$⊢ φ \to (M \dots N) = (M ..^N + 1)$
13	12	sumeq1d	$⊢ φ \to \sum_{k = M}^{N} A = \sum_{k \in (M ..^N + 1)} A$
14	9 10 13	3eqtr2rd	$⊢ φ \to \sum_{k \in (M ..^N + 1)} A = \sum_{k \in (M ..^N)} A + B$

Metamath Proof Explorer