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={\mathbb{Z}}_{\ge M}$$
	isumclim.2	$$⊢\phi \to M\in \mathbb{Z}$$
	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 seqM\left(+,F\right)\in \mathrm{dom}⇝$$
Assertion	isumclim2	$$⊢\phi \to seqM\left(+,F\right)⇝\sum _{k\in Z}A$$

Proof

Step	Hyp	Ref	Expression
1		isumclim.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
2		isumclim.2	$$⊢\phi \to M\in \mathbb{Z}$$
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 seqM\left(+,F\right)\in \mathrm{dom}⇝$$
6		climdm	$$⊢seqM\left(+,F\right)\in \mathrm{dom}⇝\leftrightarrow seqM\left(+,F\right)⇝⇝\left(seqM\left(+,F\right)\right)$$
7	5 6	sylib	$$⊢\phi \to seqM\left(+,F\right)⇝⇝\left(seqM\left(+,F\right)\right)$$
8	1 2 3 4	isum	$$⊢\phi \to \sum _{k\in Z}A=⇝\left(seqM\left(+,F\right)\right)$$
9	7 8	breqtrrd	$$⊢\phi \to seqM\left(+,F\right)⇝\sum _{k\in Z}A$$