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 = ( ZZ>= ` M )
	isumcl.2	|- ( ph -> M e. ZZ )
	isumcl.3	|- ( ( ph /\ k e. Z ) -> ( F ` k ) = A )
	isumcl.4	|- ( ( ph /\ k e. Z ) -> A e. CC )
	isumcl.5	|- ( ph -> seq M ( + , F ) e. dom ~~> )
Assertion	isumcl	|- ( ph -> sum_ k e. Z A e. CC )

Proof

Step	Hyp	Ref	Expression
1		isumcl.1	|- Z = ( ZZ>= ` M )
2		isumcl.2	|- ( ph -> M e. ZZ )
3		isumcl.3	|- ( ( ph /\ k e. Z ) -> ( F ` k ) = A )
4		isumcl.4	|- ( ( ph /\ k e. Z ) -> A e. CC )
5		isumcl.5	|- ( ph -> seq M ( + , F ) e. dom ~~> )
6	1 2 3 4	isum	|- ( ph -> sum_ k e. Z A = ( ~~> ` seq M ( + , F ) ) )
7		fclim	|- ~~> : dom ~~> --> CC
8		ffvelrn	|- ( ( ~~> : dom ~~> --> CC /\ seq M ( + , F ) e. dom ~~> ) -> ( ~~> ` seq M ( + , F ) ) e. CC )
9	7 5 8	sylancr	|- ( ph -> ( ~~> ` seq M ( + , F ) ) e. CC )
10	6 9	eqeltrd	|- ( ph -> sum_ k e. Z A e. CC )