Metamath Proof Explorer

Theorem fzosump1

Description: Separate out the last term in a finite sum. (Contributed by Mario Carneiro, 13-Apr-2016)

Ref Expression
Hypotheses fsumm1.1 
|- ( ph -> N e. ( ZZ>= ` M ) )
fsumm1.2 
|- ( ( ph /\ k e. ( M ... N ) ) -> A e. CC )
fsumm1.3 
|- ( k = N -> A = B )
Assertion fzosump1 
|- ( ph -> sum_ k e. ( M ..^ ( N + 1 ) ) A = ( sum_ k e. ( M ..^ N ) A + B ) )

Proof

Step Hyp Ref Expression
1 fsumm1.1 
 |-  ( ph -> N e. ( ZZ>= ` M ) )
2 fsumm1.2 
 |-  ( ( ph /\ k e. ( M ... N ) ) -> A e. CC )
3 fsumm1.3 
 |-  ( k = N -> A = B )
4 eluzelz 
 |-  ( N e. ( ZZ>= ` M ) -> N e. ZZ )
5 1 4 syl 
 |-  ( ph -> N e. ZZ )
6 fzoval 
 |-  ( N e. ZZ -> ( M ..^ N ) = ( M ... ( N - 1 ) ) )
7 5 6 syl 
 |-  ( ph -> ( M ..^ N ) = ( M ... ( N - 1 ) ) )
8 7 sumeq1d 
 |-  ( ph -> sum_ k e. ( M ..^ N ) A = sum_ k e. ( M ... ( N - 1 ) ) A )
9 8 oveq1d 
 |-  ( ph -> ( sum_ k e. ( M ..^ N ) A + B ) = ( sum_ k e. ( M ... ( N - 1 ) ) A + B ) )
10 1 2 3 fsumm1 
 |-  ( ph -> sum_ k e. ( M ... N ) A = ( sum_ k e. ( M ... ( N - 1 ) ) A + B ) )
11 fzval3 
 |-  ( N e. ZZ -> ( M ... N ) = ( M ..^ ( N + 1 ) ) )
12 5 11 syl 
 |-  ( ph -> ( M ... N ) = ( M ..^ ( N + 1 ) ) )
13 12 sumeq1d 
 |-  ( ph -> sum_ k e. ( M ... N ) A = sum_ k e. ( M ..^ ( N + 1 ) ) A )
14 9 10 13 3eqtr2rd 
 |-  ( ph -> sum_ k e. ( M ..^ ( N + 1 ) ) A = ( sum_ k e. ( M ..^ N ) A + B ) )