Theorem isumcl

Description: The sum of a converging infinite series is a complex number. (Contributed by NM, 13-Dec-2005) (Revised by Mario Carneiro, 23-Apr-2014)

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

Proof

Step	Hyp	Ref	Expression
1		isumcl.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
2		isumcl.2	$$⊢\phi \to M\in \mathbb{Z}$$
3		isumcl.3	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)=A$$
4		isumcl.4	$$⊢\left(\phi \wedge k\in Z\right)\to A\in ℂ$$
5		isumcl.5	$$⊢\phi \to seqM\left(+,F\right)\in \mathrm{dom}⇝$$
6	1 2 3 4	isum	$$⊢\phi \to \sum _{k\in Z}A=⇝\left(seqM\left(+,F\right)\right)$$
7		fclim	$$⊢⇝:\mathrm{dom}⇝⟶ℂ$$
8		ffvelrn	$$⊢\left(⇝:\mathrm{dom}⇝⟶ℂ\wedge seqM\left(+,F\right)\in \mathrm{dom}⇝\right)\to ⇝\left(seqM\left(+,F\right)\right)\in ℂ$$
9	7 5 8	sylancr	$$⊢\phi \to ⇝\left(seqM\left(+,F\right)\right)\in ℂ$$
10	6 9	eqeltrd	$$⊢\phi \to \sum _{k\in Z}A\in ℂ$$