# Metamath Proof Explorer

## Theorem fsump1i

Description: Optimized version of fsump1 for making sums of a concrete number of terms. (Contributed by Mario Carneiro, 23-Apr-2014)

Ref Expression
Hypotheses fsump1i.1 ${⊢}{Z}={ℤ}_{\ge {M}}$
fsump1i.2 ${⊢}{N}={K}+1$
fsump1i.3 ${⊢}{k}={N}\to {A}={B}$
fsump1i.4 ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {A}\in ℂ$
fsump1i.5 ${⊢}{\phi }\to \left({K}\in {Z}\wedge \sum _{{k}={M}}^{{K}}{A}={S}\right)$
fsump1i.6 ${⊢}{\phi }\to {S}+{B}={T}$
Assertion fsump1i ${⊢}{\phi }\to \left({N}\in {Z}\wedge \sum _{{k}={M}}^{{N}}{A}={T}\right)$

### Proof

Step Hyp Ref Expression
1 fsump1i.1 ${⊢}{Z}={ℤ}_{\ge {M}}$
2 fsump1i.2 ${⊢}{N}={K}+1$
3 fsump1i.3 ${⊢}{k}={N}\to {A}={B}$
4 fsump1i.4 ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {A}\in ℂ$
5 fsump1i.5 ${⊢}{\phi }\to \left({K}\in {Z}\wedge \sum _{{k}={M}}^{{K}}{A}={S}\right)$
6 fsump1i.6 ${⊢}{\phi }\to {S}+{B}={T}$
7 5 simpld ${⊢}{\phi }\to {K}\in {Z}$
8 7 1 eleqtrdi ${⊢}{\phi }\to {K}\in {ℤ}_{\ge {M}}$
9 peano2uz ${⊢}{K}\in {ℤ}_{\ge {M}}\to {K}+1\in {ℤ}_{\ge {M}}$
10 9 1 eleqtrrdi ${⊢}{K}\in {ℤ}_{\ge {M}}\to {K}+1\in {Z}$
11 8 10 syl ${⊢}{\phi }\to {K}+1\in {Z}$
12 2 11 eqeltrid ${⊢}{\phi }\to {N}\in {Z}$
13 2 oveq2i ${⊢}\left({M}\dots {N}\right)=\left({M}\dots {K}+1\right)$
14 13 sumeq1i ${⊢}\sum _{{k}={M}}^{{N}}{A}=\sum _{{k}={M}}^{{K}+1}{A}$
15 elfzuz ${⊢}{k}\in \left({M}\dots {K}+1\right)\to {k}\in {ℤ}_{\ge {M}}$
16 15 1 eleqtrrdi ${⊢}{k}\in \left({M}\dots {K}+1\right)\to {k}\in {Z}$
17 16 4 sylan2 ${⊢}\left({\phi }\wedge {k}\in \left({M}\dots {K}+1\right)\right)\to {A}\in ℂ$
18 2 eqeq2i ${⊢}{k}={N}↔{k}={K}+1$
19 18 3 sylbir ${⊢}{k}={K}+1\to {A}={B}$
20 8 17 19 fsump1 ${⊢}{\phi }\to \sum _{{k}={M}}^{{K}+1}{A}=\sum _{{k}={M}}^{{K}}{A}+{B}$
21 14 20 syl5eq ${⊢}{\phi }\to \sum _{{k}={M}}^{{N}}{A}=\sum _{{k}={M}}^{{K}}{A}+{B}$
22 5 simprd ${⊢}{\phi }\to \sum _{{k}={M}}^{{K}}{A}={S}$
23 22 oveq1d ${⊢}{\phi }\to \sum _{{k}={M}}^{{K}}{A}+{B}={S}+{B}$
24 21 23 6 3eqtrd ${⊢}{\phi }\to \sum _{{k}={M}}^{{N}}{A}={T}$
25 12 24 jca ${⊢}{\phi }\to \left({N}\in {Z}\wedge \sum _{{k}={M}}^{{N}}{A}={T}\right)$