# Metamath Proof Explorer

## Theorem isumclim2

Description: A converging series converges to its infinite sum. (Contributed by NM, 2-Jan-2006) (Revised by Mario Carneiro, 23-Apr-2014)

Ref Expression
Hypotheses isumclim.1 ${⊢}{Z}={ℤ}_{\ge {M}}$
isumclim.2 ${⊢}{\phi }\to {M}\in ℤ$
isumclim.3 ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {F}\left({k}\right)={A}$
isumclim.4 ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {A}\in ℂ$
isumclim2.5 ${⊢}{\phi }\to seq{M}\left(+,{F}\right)\in \mathrm{dom}⇝$
Assertion isumclim2 ${⊢}{\phi }\to seq{M}\left(+,{F}\right)⇝\sum _{{k}\in {Z}}{A}$

### Proof

Step Hyp Ref Expression
1 isumclim.1 ${⊢}{Z}={ℤ}_{\ge {M}}$
2 isumclim.2 ${⊢}{\phi }\to {M}\in ℤ$
3 isumclim.3 ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {F}\left({k}\right)={A}$
4 isumclim.4 ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {A}\in ℂ$
5 isumclim2.5 ${⊢}{\phi }\to seq{M}\left(+,{F}\right)\in \mathrm{dom}⇝$
6 climdm ${⊢}seq{M}\left(+,{F}\right)\in \mathrm{dom}⇝↔seq{M}\left(+,{F}\right)⇝⇝\left(seq{M}\left(+,{F}\right)\right)$
7 5 6 sylib ${⊢}{\phi }\to seq{M}\left(+,{F}\right)⇝⇝\left(seq{M}\left(+,{F}\right)\right)$
8 1 2 3 4 isum ${⊢}{\phi }\to \sum _{{k}\in {Z}}{A}=⇝\left(seq{M}\left(+,{F}\right)\right)$
9 7 8 breqtrrd ${⊢}{\phi }\to seq{M}\left(+,{F}\right)⇝\sum _{{k}\in {Z}}{A}$