Theorem isumrecl

Description: The sum of a converging infinite real series is a real number. (Contributed by Mario Carneiro, 24-Apr-2014)

	Ref	Expression
Hypotheses	isumrecl.1	|- Z = ( ZZ>= ` M )
	isumrecl.2	|- ( ph -> M e. ZZ )
	isumrecl.3	|- ( ( ph /\ k e. Z ) -> ( F ` k ) = A )
	isumrecl.4	|- ( ( ph /\ k e. Z ) -> A e. RR )
	isumrecl.5	|- ( ph -> seq M ( + , F ) e. dom ~~> )
Assertion	isumrecl	|- ( ph -> sum_ k e. Z A e. RR )

Proof

Step	Hyp	Ref	Expression
1		isumrecl.1	|- Z = ( ZZ>= ` M )
2		isumrecl.2	|- ( ph -> M e. ZZ )
3		isumrecl.3	|- ( ( ph /\ k e. Z ) -> ( F ` k ) = A )
4		isumrecl.4	|- ( ( ph /\ k e. Z ) -> A e. RR )
5		isumrecl.5	|- ( ph -> seq M ( + , F ) e. dom ~~> )
6	4	recnd	|- ( ( ph /\ k e. Z ) -> A e. CC )
7	1 2 3 6 5	isumclim2	|- ( ph -> seq M ( + , F ) ~~> sum_ k e. Z A )
8	3 4	eqeltrd	|- ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )
9	1 2 8	serfre	|- ( ph -> seq M ( + , F ) : Z --> RR )
10	9	ffvelrnda	|- ( ( ph /\ j e. Z ) -> ( seq M ( + , F ) ` j ) e. RR )
11	1 2 7 10	climrecl	|- ( ph -> sum_ k e. Z A e. RR )