Theorem fzosumm1

Description: Separate out the last term in a finite sum. (Contributed by Steven Nguyen, 22-Aug-2023)

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

Proof

Step	Hyp	Ref	Expression
1		fzosumm1.1	$$⊢\phi \to N-1\in {\mathbb{Z}}_{\ge M}$$
2		fzosumm1.2	$$⊢\left(\phi \wedge k\in \left(M..^N\right)\right)\to A\in ℂ$$
3		fzosumm1.3	$$⊢k=N-1\to A=B$$
4		fzosumm1.n	$$⊢\phi \to N\in \mathbb{Z}$$
5		fzoval	$$⊢N\in \mathbb{Z}\to \left(M..^N\right)=\left(M\dots N-1\right)$$
6	4 5	syl	$$⊢\phi \to \left(M..^N\right)=\left(M\dots N-1\right)$$
7	6	eqcomd	$$⊢\phi \to \left(M\dots N-1\right)=\left(M..^N\right)$$
8	7	eleq2d	$$⊢\phi \to \left(k\in \left(M\dots N-1\right)\leftrightarrow k\in \left(M..^N\right)\right)$$
9	8	biimpa	$$⊢\left(\phi \wedge k\in \left(M\dots N-1\right)\right)\to k\in \left(M..^N\right)$$
10	9 2	syldan	$$⊢\left(\phi \wedge k\in \left(M\dots N-1\right)\right)\to A\in ℂ$$
11	1 10 3	fsumm1	$$⊢\phi \to \sum _{k=M}^{N-1}A=\sum _{k=M}^{N-1-1}A+B$$
12	6	sumeq1d	$$⊢\phi \to \sum _{k\in \left(M..^N\right)}A=\sum _{k=M}^{N-1}A$$
13		eluzelz	$$⊢N-1\in {\mathbb{Z}}_{\ge M}\to N-1\in \mathbb{Z}$$
14		fzoval	$$⊢N-1\in \mathbb{Z}\to \left(M..^N-1\right)=\left(M\dots N-1-1\right)$$
15	1 13 14	3syl	$$⊢\phi \to \left(M..^N-1\right)=\left(M\dots N-1-1\right)$$
16	15	sumeq1d	$$⊢\phi \to \sum _{k\in \left(M..^N-1\right)}A=\sum _{k=M}^{N-1-1}A$$
17	16	oveq1d	$$⊢\phi \to \sum _{k\in \left(M..^N-1\right)}A+B=\sum _{k=M}^{N-1-1}A+B$$
18	11 12 17	3eqtr4d	$$⊢\phi \to \sum _{k\in \left(M..^N\right)}A=\sum _{k\in \left(M..^N-1\right)}A+B$$