Metamath Proof Explorer

Theorem fsumsers

Description: Special case of series sum over a finite upper integer index set. (Contributed by Mario Carneiro, 26-Jul-2013) (Revised by Mario Carneiro, 21-Apr-2014)

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

Proof

Step Hyp Ref Expression
1 fsumsers.1 
 |-  ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( F ` k ) = if ( k e. A , B , 0 ) )
2 fsumsers.2 
 |-  ( ph -> N e. ( ZZ>= ` M ) )
3 fsumsers.3 
 |-  ( ( ph /\ k e. A ) -> B e. CC )
4 fsumsers.4 
 |-  ( ph -> A C_ ( M ... N ) )
5 eqid 
 |-  ( ZZ>= ` M ) = ( ZZ>= ` M )
6 eluzel2 
 |-  ( N e. ( ZZ>= ` M ) -> M e. ZZ )
7 2 6 syl 
 |-  ( ph -> M e. ZZ )
8 fzssuz 
 |-  ( M ... N ) C_ ( ZZ>= ` M )
9 4 8 sstrdi 
 |-  ( ph -> A C_ ( ZZ>= ` M ) )
10 5 7 9 1 3 zsum 
 |-  ( ph -> sum_ k e. A B = ( ~~> ` seq M ( + , F ) ) )
11 fclim 
 |-  ~~> : dom ~~> --> CC
12 ffun 
 |-  ( ~~> : dom ~~> --> CC -> Fun ~~> )
13 11 12 ax-mp 
 |-  Fun ~~>
14 1 2 3 4 fsumcvg2 
 |-  ( ph -> seq M ( + , F ) ~~> ( seq M ( + , F ) ` N ) )
15 funbrfv 
 |-  ( Fun ~~> -> ( seq M ( + , F ) ~~> ( seq M ( + , F ) ` N ) -> ( ~~> ` seq M ( + , F ) ) = ( seq M ( + , F ) ` N ) ) )
16 13 14 15 mpsyl 
 |-  ( ph -> ( ~~> ` seq M ( + , F ) ) = ( seq M ( + , F ) ` N ) )
17 10 16 eqtrd 
 |-  ( ph -> sum_ k e. A B = ( seq M ( + , F ) ` N ) )