# Metamath Proof Explorer

## 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 {ℤ}_{\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 {ℤ}_{\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 {ℤ}_{\ge {M}}\to {N}\in ℤ$
5 1 4 syl ${⊢}{\phi }\to {N}\in ℤ$
6 fzoval ${⊢}{N}\in ℤ\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 ℤ\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}$