# Metamath Proof Explorer

## Theorem fsumsers

Description: Special case of series sum over a finite upper integer index set. (Contributed by Mario Carneiro, 26-Jul-2013) (Revised by Mario Carneiro, 21-Apr-2014)

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

### Proof

Step Hyp Ref Expression
1 fsumsers.1 ${⊢}\left({\phi }\wedge {k}\in {ℤ}_{\ge {M}}\right)\to {F}\left({k}\right)=if\left({k}\in {A},{B},0\right)$
2 fsumsers.2 ${⊢}{\phi }\to {N}\in {ℤ}_{\ge {M}}$
3 fsumsers.3 ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {B}\in ℂ$
4 fsumsers.4 ${⊢}{\phi }\to {A}\subseteq \left({M}\dots {N}\right)$
5 eqid ${⊢}{ℤ}_{\ge {M}}={ℤ}_{\ge {M}}$
6 eluzel2 ${⊢}{N}\in {ℤ}_{\ge {M}}\to {M}\in ℤ$
7 2 6 syl ${⊢}{\phi }\to {M}\in ℤ$
8 fzssuz ${⊢}\left({M}\dots {N}\right)\subseteq {ℤ}_{\ge {M}}$
9 4 8 sstrdi ${⊢}{\phi }\to {A}\subseteq {ℤ}_{\ge {M}}$
10 5 7 9 1 3 zsum ${⊢}{\phi }\to \sum _{{k}\in {A}}{B}=⇝\left(seq{M}\left(+,{F}\right)\right)$
11 fclim ${⊢}⇝:\mathrm{dom}⇝⟶ℂ$
12 ffun ${⊢}⇝:\mathrm{dom}⇝⟶ℂ\to \mathrm{Fun}⇝$
13 11 12 ax-mp ${⊢}\mathrm{Fun}⇝$
14 1 2 3 4 fsumcvg2 ${⊢}{\phi }\to seq{M}\left(+,{F}\right)⇝seq{M}\left(+,{F}\right)\left({N}\right)$
15 funbrfv ${⊢}\mathrm{Fun}⇝\to \left(seq{M}\left(+,{F}\right)⇝seq{M}\left(+,{F}\right)\left({N}\right)\to ⇝\left(seq{M}\left(+,{F}\right)\right)=seq{M}\left(+,{F}\right)\left({N}\right)\right)$
16 13 14 15 mpsyl ${⊢}{\phi }\to ⇝\left(seq{M}\left(+,{F}\right)\right)=seq{M}\left(+,{F}\right)\left({N}\right)$
17 10 16 eqtrd ${⊢}{\phi }\to \sum _{{k}\in {A}}{B}=seq{M}\left(+,{F}\right)\left({N}\right)$