# Metamath Proof Explorer

## Theorem fsumser

Description: A finite sum expressed in terms of a partial sum of an infinite series. The recursive definition follows as fsum1 and fsump1i , which should make our notation clear and from which, along with closure fsumcl , we will derive the basic properties of finite sums. (Contributed by NM, 11-Dec-2005) (Revised by Mario Carneiro, 21-Apr-2014)

Ref Expression
Hypotheses fsumser.1 ${⊢}\left({\phi }\wedge {k}\in \left({M}\dots {N}\right)\right)\to {F}\left({k}\right)={A}$
fsumser.2 ${⊢}{\phi }\to {N}\in {ℤ}_{\ge {M}}$
fsumser.3 ${⊢}\left({\phi }\wedge {k}\in \left({M}\dots {N}\right)\right)\to {A}\in ℂ$
Assertion fsumser ${⊢}{\phi }\to \sum _{{k}={M}}^{{N}}{A}=seq{M}\left(+,{F}\right)\left({N}\right)$

### Proof

Step Hyp Ref Expression
1 fsumser.1 ${⊢}\left({\phi }\wedge {k}\in \left({M}\dots {N}\right)\right)\to {F}\left({k}\right)={A}$
2 fsumser.2 ${⊢}{\phi }\to {N}\in {ℤ}_{\ge {M}}$
3 fsumser.3 ${⊢}\left({\phi }\wedge {k}\in \left({M}\dots {N}\right)\right)\to {A}\in ℂ$
4 eleq1w ${⊢}{m}={k}\to \left({m}\in \left({M}\dots {N}\right)↔{k}\in \left({M}\dots {N}\right)\right)$
5 fveq2 ${⊢}{m}={k}\to {F}\left({m}\right)={F}\left({k}\right)$
6 4 5 ifbieq1d ${⊢}{m}={k}\to if\left({m}\in \left({M}\dots {N}\right),{F}\left({m}\right),0\right)=if\left({k}\in \left({M}\dots {N}\right),{F}\left({k}\right),0\right)$
7 eqid ${⊢}\left({m}\in {ℤ}_{\ge {M}}⟼if\left({m}\in \left({M}\dots {N}\right),{F}\left({m}\right),0\right)\right)=\left({m}\in {ℤ}_{\ge {M}}⟼if\left({m}\in \left({M}\dots {N}\right),{F}\left({m}\right),0\right)\right)$
8 fvex ${⊢}{F}\left({k}\right)\in \mathrm{V}$
9 c0ex ${⊢}0\in \mathrm{V}$
10 8 9 ifex ${⊢}if\left({k}\in \left({M}\dots {N}\right),{F}\left({k}\right),0\right)\in \mathrm{V}$
11 6 7 10 fvmpt ${⊢}{k}\in {ℤ}_{\ge {M}}\to \left({m}\in {ℤ}_{\ge {M}}⟼if\left({m}\in \left({M}\dots {N}\right),{F}\left({m}\right),0\right)\right)\left({k}\right)=if\left({k}\in \left({M}\dots {N}\right),{F}\left({k}\right),0\right)$
12 1 ifeq1da ${⊢}{\phi }\to if\left({k}\in \left({M}\dots {N}\right),{F}\left({k}\right),0\right)=if\left({k}\in \left({M}\dots {N}\right),{A},0\right)$
13 11 12 sylan9eqr ${⊢}\left({\phi }\wedge {k}\in {ℤ}_{\ge {M}}\right)\to \left({m}\in {ℤ}_{\ge {M}}⟼if\left({m}\in \left({M}\dots {N}\right),{F}\left({m}\right),0\right)\right)\left({k}\right)=if\left({k}\in \left({M}\dots {N}\right),{A},0\right)$
14 ssidd ${⊢}{\phi }\to \left({M}\dots {N}\right)\subseteq \left({M}\dots {N}\right)$
15 13 2 3 14 fsumsers ${⊢}{\phi }\to \sum _{{k}={M}}^{{N}}{A}=seq{M}\left(+,\left({m}\in {ℤ}_{\ge {M}}⟼if\left({m}\in \left({M}\dots {N}\right),{F}\left({m}\right),0\right)\right)\right)\left({N}\right)$
16 elfzuz ${⊢}{k}\in \left({M}\dots {N}\right)\to {k}\in {ℤ}_{\ge {M}}$
17 16 11 syl ${⊢}{k}\in \left({M}\dots {N}\right)\to \left({m}\in {ℤ}_{\ge {M}}⟼if\left({m}\in \left({M}\dots {N}\right),{F}\left({m}\right),0\right)\right)\left({k}\right)=if\left({k}\in \left({M}\dots {N}\right),{F}\left({k}\right),0\right)$
18 iftrue ${⊢}{k}\in \left({M}\dots {N}\right)\to if\left({k}\in \left({M}\dots {N}\right),{F}\left({k}\right),0\right)={F}\left({k}\right)$
19 17 18 eqtrd ${⊢}{k}\in \left({M}\dots {N}\right)\to \left({m}\in {ℤ}_{\ge {M}}⟼if\left({m}\in \left({M}\dots {N}\right),{F}\left({m}\right),0\right)\right)\left({k}\right)={F}\left({k}\right)$
20 19 adantl ${⊢}\left({\phi }\wedge {k}\in \left({M}\dots {N}\right)\right)\to \left({m}\in {ℤ}_{\ge {M}}⟼if\left({m}\in \left({M}\dots {N}\right),{F}\left({m}\right),0\right)\right)\left({k}\right)={F}\left({k}\right)$
21 2 20 seqfveq ${⊢}{\phi }\to seq{M}\left(+,\left({m}\in {ℤ}_{\ge {M}}⟼if\left({m}\in \left({M}\dots {N}\right),{F}\left({m}\right),0\right)\right)\right)\left({N}\right)=seq{M}\left(+,{F}\right)\left({N}\right)$
22 15 21 eqtrd ${⊢}{\phi }\to \sum _{{k}={M}}^{{N}}{A}=seq{M}\left(+,{F}\right)\left({N}\right)$