Theorem fzosump1

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

	Ref	Expression
Hypotheses	fsumm1.1	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge M}$$
	fsumm1.2	$$⊢\left(\phi \wedge k\in \left(M\dots N\right)\right)\to A\in ℂ$$
	fsumm1.3	$$⊢k=N\to A=B$$
Assertion	fzosump1	$$⊢\phi \to \sum _{k\in \left(M..^N+1\right)}A=\sum _{k\in \left(M..^N\right)}A+B$$

Proof

Step	Hyp	Ref	Expression
1		fsumm1.1	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge M}$$
2		fsumm1.2	$$⊢\left(\phi \wedge k\in \left(M\dots N\right)\right)\to A\in ℂ$$
3		fsumm1.3	$$⊢k=N\to A=B$$
4		eluzelz	$$⊢N\in {\mathbb{Z}}_{\ge M}\to N\in \mathbb{Z}$$
5	1 4	syl	$$⊢\phi \to N\in \mathbb{Z}$$
6		fzoval	$$⊢N\in \mathbb{Z}\to \left(M..^N\right)=\left(M\dots N-1\right)$$
7	5 6	syl	$$⊢\phi \to \left(M..^N\right)=\left(M\dots N-1\right)$$
8	7	sumeq1d	$$⊢\phi \to \sum _{k\in \left(M..^N\right)}A=\sum _{k=M}^{N-1}A$$
9	8	oveq1d	$$⊢\phi \to \sum _{k\in \left(M..^N\right)}A+B=\sum _{k=M}^{N-1}A+B$$
10	1 2 3	fsumm1	$$⊢\phi \to \sum _{k=M}^{N}A=\sum _{k=M}^{N-1}A+B$$
11		fzval3	$$⊢N\in \mathbb{Z}\to \left(M\dots N\right)=\left(M..^N+1\right)$$
12	5 11	syl	$$⊢\phi \to \left(M\dots N\right)=\left(M..^N+1\right)$$
13	12	sumeq1d	$$⊢\phi \to \sum _{k=M}^{N}A=\sum _{k\in \left(M..^N+1\right)}A$$
14	9 10 13	3eqtr2rd	$$⊢\phi \to \sum _{k\in \left(M..^N+1\right)}A=\sum _{k\in \left(M..^N\right)}A+B$$