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 = ( 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 )
	isumclim.6	|- ( ph -> seq M ( + , F ) ~~> B )
Assertion	isumclim	|- ( ph -> sum_ k e. Z A = B )

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		isumclim.6	|- ( ph -> seq M ( + , F ) ~~> B )
6	1 2 3 4	isum	|- ( ph -> sum_ k e. Z A = ( ~~> ` seq M ( + , F ) ) )
7		fclim	|- ~~> : dom ~~> --> CC
8		ffun	|- ( ~~> : dom ~~> --> CC -> Fun ~~> )
9	7 8	ax-mp	|- Fun ~~>
10		funbrfv	|- ( Fun ~~> -> ( seq M ( + , F ) ~~> B -> ( ~~> ` seq M ( + , F ) ) = B ) )
11	9 5 10	mpsyl	|- ( ph -> ( ~~> ` seq M ( + , F ) ) = B )
12	6 11	eqtrd	|- ( ph -> sum_ k e. Z A = B )