Theorem isumclim

Description: An infinite sum equals the value its series converges to. (Contributed by NM, 25-Dec-2005) (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 ℂ$$
	isumclim.6	$$⊢\phi \to seqM\left(+,F\right)⇝B$$
Assertion	isumclim	$$⊢\phi \to \sum _{k\in Z}A=B$$

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		isumclim.6	$$⊢\phi \to seqM\left(+,F\right)⇝B$$
6	1 2 3 4	isum	$$⊢\phi \to \sum _{k\in Z}A=⇝\left(seqM\left(+,F\right)\right)$$
7		fclim	$$⊢⇝:\mathrm{dom}⇝⟶ℂ$$
8		ffun	$$⊢⇝:\mathrm{dom}⇝⟶ℂ\to \mathrm{Fun}⇝$$
9	7 8	ax-mp	$$⊢\mathrm{Fun}⇝$$
10		funbrfv	$$⊢\mathrm{Fun}⇝\to \left(seqM\left(+,F\right)⇝B\to ⇝\left(seqM\left(+,F\right)\right)=B\right)$$
11	9 5 10	mpsyl	$$⊢\phi \to ⇝\left(seqM\left(+,F\right)\right)=B$$
12	6 11	eqtrd	$$⊢\phi \to \sum _{k\in Z}A=B$$