This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )