Theorem fsumser

Description: A finite sum expressed in terms of a partial sum of an infinite series. The recursive definition follows as fsum1 and fsump1i , which should make our notation clear and from which, along with closure fsumcl , we will derive the basic properties of finite sums. (Contributed by NM, 11-Dec-2005) (Revised by Mario Carneiro, 21-Apr-2014)

	Ref	Expression
Hypotheses	fsumser.1	|- ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) = A )
	fsumser.2	|- ( ph -> N e. ( ZZ>= ` M ) )
	fsumser.3	|- ( ( ph /\ k e. ( M ... N ) ) -> A e. CC )
Assertion	fsumser	|- ( ph -> sum_ k e. ( M ... N ) A = ( seq M ( + , F ) ` N ) )

Proof

Step	Hyp	Ref	Expression
1		fsumser.1	|- ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) = A )
2		fsumser.2	|- ( ph -> N e. ( ZZ>= ` M ) )
3		fsumser.3	|- ( ( ph /\ k e. ( M ... N ) ) -> A e. CC )
4		eleq1w	|- ( m = k -> ( m e. ( M ... N ) <-> k e. ( M ... N ) ) )
5		fveq2	|- ( m = k -> ( F ` m ) = ( F ` k ) )
6	4 5	ifbieq1d	|- ( m = k -> if ( m e. ( M ... N ) , ( F ` m ) , 0 ) = if ( k e. ( M ... N ) , ( F ` k ) , 0 ) )
7		eqid	|- ( m e. ( ZZ>= ` M ) |-> if ( m e. ( M ... N ) , ( F ` m ) , 0 ) ) = ( m e. ( ZZ>= ` M ) |-> if ( m e. ( M ... N ) , ( F ` m ) , 0 ) )
8		fvex	|- ( F ` k ) e. _V
9		c0ex	|- 0 e. _V
10	8 9	ifex	|- if ( k e. ( M ... N ) , ( F ` k ) , 0 ) e. _V
11	6 7 10	fvmpt	|- ( k e. ( ZZ>= ` M ) -> ( ( m e. ( ZZ>= ` M ) |-> if ( m e. ( M ... N ) , ( F ` m ) , 0 ) ) ` k ) = if ( k e. ( M ... N ) , ( F ` k ) , 0 ) )
12	1	ifeq1da	|- ( ph -> if ( k e. ( M ... N ) , ( F ` k ) , 0 ) = if ( k e. ( M ... N ) , A , 0 ) )
13	11 12	sylan9eqr	|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( ( m e. ( ZZ>= ` M ) |-> if ( m e. ( M ... N ) , ( F ` m ) , 0 ) ) ` k ) = if ( k e. ( M ... N ) , A , 0 ) )
14		ssidd	|- ( ph -> ( M ... N ) C_ ( M ... N ) )
15	13 2 3 14	fsumsers	|- ( ph -> sum_ k e. ( M ... N ) A = ( seq M ( + , ( m e. ( ZZ>= ` M ) |-> if ( m e. ( M ... N ) , ( F ` m ) , 0 ) ) ) ` N ) )
16		elfzuz	|- ( k e. ( M ... N ) -> k e. ( ZZ>= ` M ) )
17	16 11	syl	|- ( k e. ( M ... N ) -> ( ( m e. ( ZZ>= ` M ) |-> if ( m e. ( M ... N ) , ( F ` m ) , 0 ) ) ` k ) = if ( k e. ( M ... N ) , ( F ` k ) , 0 ) )
18		iftrue	|- ( k e. ( M ... N ) -> if ( k e. ( M ... N ) , ( F ` k ) , 0 ) = ( F ` k ) )
19	17 18	eqtrd	|- ( k e. ( M ... N ) -> ( ( m e. ( ZZ>= ` M ) |-> if ( m e. ( M ... N ) , ( F ` m ) , 0 ) ) ` k ) = ( F ` k ) )
20	19	adantl	|- ( ( ph /\ k e. ( M ... N ) ) -> ( ( m e. ( ZZ>= ` M ) |-> if ( m e. ( M ... N ) , ( F ` m ) , 0 ) ) ` k ) = ( F ` k ) )
21	2 20	seqfveq	|- ( ph -> ( seq M ( + , ( m e. ( ZZ>= ` M ) |-> if ( m e. ( M ... N ) , ( F ` m ) , 0 ) ) ) ` N ) = ( seq M ( + , F ) ` N ) )
22	15 21	eqtrd	|- ( ph -> sum_ k e. ( M ... N ) A = ( seq M ( + , F ) ` N ) )