# 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 ) )`
` |-  ( ( ph /\ k e. ( M ... N ) ) -> ( ( m e. ( ZZ>= ` M ) |-> if ( m e. ( M ... N ) , ( F ` m ) , 0 ) ) ` k ) = ( F ` k ) )`
` |-  ( ph -> ( seq M ( + , ( m e. ( ZZ>= ` M ) |-> if ( m e. ( M ... N ) , ( F ` m ) , 0 ) ) ) ` N ) = ( seq M ( + , F ) ` N ) )`
` |-  ( ph -> sum_ k e. ( M ... N ) A = ( seq M ( + , F ) ` N ) )`