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

Proof

Step	Hyp	Ref	Expression
1		isumclim.1	|- Z = ( ZZ>= ` M )
2		isumclim.2	|- ( ph -> M e. ZZ )
3		isumclim.3	|- ( ( ph /\ k e. Z ) -> ( F ` k ) = A )
4		isumclim.4	|- ( ( ph /\ k e. Z ) -> A e. CC )
5		isumclim2.5	|- ( ph -> seq M ( + , F ) e. dom ~~> )
6		climdm	|- ( seq M ( + , F ) e. dom ~~> <-> seq M ( + , F ) ~~> ( ~~> ` seq M ( + , F ) ) )
7	5 6	sylib	|- ( ph -> seq M ( + , F ) ~~> ( ~~> ` seq M ( + , F ) ) )
8	1 2 3 4	isum	|- ( ph -> sum_ k e. Z A = ( ~~> ` seq M ( + , F ) ) )
9	7 8	breqtrrd	|- ( ph -> seq M ( + , F ) ~~> sum_ k e. Z A )