Theorem isum

Description: Series sum with an upper integer index set (i.e. an infinite series). (Contributed by Mario Carneiro, 15-Jul-2013) (Revised by Mario Carneiro, 7-Apr-2014)

	Ref	Expression
Hypotheses	zsum.1	|- Z = ( ZZ>= ` M )
	zsum.2	|- ( ph -> M e. ZZ )
	isum.3	|- ( ( ph /\ k e. Z ) -> ( F ` k ) = B )
	isum.4	|- ( ( ph /\ k e. Z ) -> B e. CC )
Assertion	isum	|- ( ph -> sum_ k e. Z B = ( ~~> ` seq M ( + , F ) ) )

Proof

Step	Hyp	Ref	Expression
1		zsum.1	|- Z = ( ZZ>= ` M )
2		zsum.2	|- ( ph -> M e. ZZ )
3		isum.3	|- ( ( ph /\ k e. Z ) -> ( F ` k ) = B )
4		isum.4	|- ( ( ph /\ k e. Z ) -> B e. CC )
5		ssidd	|- ( ph -> Z C_ Z )
6		iftrue	|- ( k e. Z -> if ( k e. Z , B , 0 ) = B )
7	6	adantl	|- ( ( ph /\ k e. Z ) -> if ( k e. Z , B , 0 ) = B )
8	3 7	eqtr4d	|- ( ( ph /\ k e. Z ) -> ( F ` k ) = if ( k e. Z , B , 0 ) )
9	1 2 5 8 4	zsum	|- ( ph -> sum_ k e. Z B = ( ~~> ` seq M ( + , F ) ) )