# Metamath Proof Explorer

## Theorem fsumcvg2

Description: The sequence of partial sums of a finite sum converges to the whole sum. (Contributed by Mario Carneiro, 20-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 fsumcvg2 ${⊢}{\phi }\to seq{M}\left(+,{F}\right)⇝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 nfcv ${⊢}\underset{_}{Ⅎ}{m}\phantom{\rule{.4em}{0ex}}if\left({k}\in {A},{B},0\right)$
6 nfv ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}{m}\in {A}$
7 nfcsb1v
8 nfcv ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}0$
9 6 7 8 nfif
10 eleq1w ${⊢}{k}={m}\to \left({k}\in {A}↔{m}\in {A}\right)$
11 csbeq1a
12 10 11 ifbieq1d
13 5 9 12 cbvmpt
14 3 ralrimiva ${⊢}{\phi }\to \forall {k}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in ℂ$
15 7 nfel1
16 11 eleq1d
17 15 16 rspc
18 14 17 mpan9
19 13 18 2 4 fsumcvg ${⊢}{\phi }\to seq{M}\left(+,\left({k}\in ℤ⟼if\left({k}\in {A},{B},0\right)\right)\right)⇝seq{M}\left(+,\left({k}\in ℤ⟼if\left({k}\in {A},{B},0\right)\right)\right)\left({N}\right)$
20 eluzel2 ${⊢}{N}\in {ℤ}_{\ge {M}}\to {M}\in ℤ$
21 2 20 syl ${⊢}{\phi }\to {M}\in ℤ$
22 eluzelz ${⊢}{k}\in {ℤ}_{\ge {M}}\to {k}\in ℤ$
23 iftrue ${⊢}{k}\in {A}\to if\left({k}\in {A},{B},0\right)={B}$
24 23 adantl ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to if\left({k}\in {A},{B},0\right)={B}$
25 24 3 eqeltrd ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to if\left({k}\in {A},{B},0\right)\in ℂ$
26 25 ex ${⊢}{\phi }\to \left({k}\in {A}\to if\left({k}\in {A},{B},0\right)\in ℂ\right)$
27 iffalse ${⊢}¬{k}\in {A}\to if\left({k}\in {A},{B},0\right)=0$
28 0cn ${⊢}0\in ℂ$
29 27 28 syl6eqel ${⊢}¬{k}\in {A}\to if\left({k}\in {A},{B},0\right)\in ℂ$
30 26 29 pm2.61d1 ${⊢}{\phi }\to if\left({k}\in {A},{B},0\right)\in ℂ$
31 eqid ${⊢}\left({k}\in ℤ⟼if\left({k}\in {A},{B},0\right)\right)=\left({k}\in ℤ⟼if\left({k}\in {A},{B},0\right)\right)$
32 31 fvmpt2 ${⊢}\left({k}\in ℤ\wedge if\left({k}\in {A},{B},0\right)\in ℂ\right)\to \left({k}\in ℤ⟼if\left({k}\in {A},{B},0\right)\right)\left({k}\right)=if\left({k}\in {A},{B},0\right)$
33 22 30 32 syl2anr ${⊢}\left({\phi }\wedge {k}\in {ℤ}_{\ge {M}}\right)\to \left({k}\in ℤ⟼if\left({k}\in {A},{B},0\right)\right)\left({k}\right)=if\left({k}\in {A},{B},0\right)$
34 1 33 eqtr4d ${⊢}\left({\phi }\wedge {k}\in {ℤ}_{\ge {M}}\right)\to {F}\left({k}\right)=\left({k}\in ℤ⟼if\left({k}\in {A},{B},0\right)\right)\left({k}\right)$
35 34 ralrimiva ${⊢}{\phi }\to \forall {k}\in {ℤ}_{\ge {M}}\phantom{\rule{.4em}{0ex}}{F}\left({k}\right)=\left({k}\in ℤ⟼if\left({k}\in {A},{B},0\right)\right)\left({k}\right)$
36 nffvmpt1 ${⊢}\underset{_}{Ⅎ}{k}\phantom{\rule{.4em}{0ex}}\left({k}\in ℤ⟼if\left({k}\in {A},{B},0\right)\right)\left({n}\right)$
37 36 nfeq2 ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}{F}\left({n}\right)=\left({k}\in ℤ⟼if\left({k}\in {A},{B},0\right)\right)\left({n}\right)$
38 fveq2 ${⊢}{k}={n}\to {F}\left({k}\right)={F}\left({n}\right)$
39 fveq2 ${⊢}{k}={n}\to \left({k}\in ℤ⟼if\left({k}\in {A},{B},0\right)\right)\left({k}\right)=\left({k}\in ℤ⟼if\left({k}\in {A},{B},0\right)\right)\left({n}\right)$
40 38 39 eqeq12d ${⊢}{k}={n}\to \left({F}\left({k}\right)=\left({k}\in ℤ⟼if\left({k}\in {A},{B},0\right)\right)\left({k}\right)↔{F}\left({n}\right)=\left({k}\in ℤ⟼if\left({k}\in {A},{B},0\right)\right)\left({n}\right)\right)$
41 37 40 rspc ${⊢}{n}\in {ℤ}_{\ge {M}}\to \left(\forall {k}\in {ℤ}_{\ge {M}}\phantom{\rule{.4em}{0ex}}{F}\left({k}\right)=\left({k}\in ℤ⟼if\left({k}\in {A},{B},0\right)\right)\left({k}\right)\to {F}\left({n}\right)=\left({k}\in ℤ⟼if\left({k}\in {A},{B},0\right)\right)\left({n}\right)\right)$
42 35 41 mpan9 ${⊢}\left({\phi }\wedge {n}\in {ℤ}_{\ge {M}}\right)\to {F}\left({n}\right)=\left({k}\in ℤ⟼if\left({k}\in {A},{B},0\right)\right)\left({n}\right)$
43 21 42 seqfeq ${⊢}{\phi }\to seq{M}\left(+,{F}\right)=seq{M}\left(+,\left({k}\in ℤ⟼if\left({k}\in {A},{B},0\right)\right)\right)$
44 43 fveq1d ${⊢}{\phi }\to seq{M}\left(+,{F}\right)\left({N}\right)=seq{M}\left(+,\left({k}\in ℤ⟼if\left({k}\in {A},{B},0\right)\right)\right)\left({N}\right)$
45 19 43 44 3brtr4d ${⊢}{\phi }\to seq{M}\left(+,{F}\right)⇝seq{M}\left(+,{F}\right)\left({N}\right)$