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

Metamath Proof Explorer

Theorem fsump1

Description: The addition of the next term in a finite sum of A ( k ) is the current term plus B i.e. A ( N + 1 ) . (Contributed by NM, 4-Nov-2005) (Revised by Mario Carneiro, 21-Apr-2014) (Proof shortened by SN, 22-Mar-2025)

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

Proof

Step Hyp Ref Expression
1 fsump1.1 
 |-  ( ph -> N e. ( ZZ>= ` M ) )
2 fsump1.2 
 |-  ( ( ph /\ k e. ( M ... ( N + 1 ) ) ) -> A e. CC )
3 fsump1.3 
 |-  ( k = ( N + 1 ) -> A = B )
4 peano2uz 
 |-  ( N e. ( ZZ>= ` M ) -> ( N + 1 ) e. ( ZZ>= ` M ) )
5 1 4 syl 
 |-  ( ph -> ( N + 1 ) e. ( ZZ>= ` M ) )
6 5 2 3 fsumm1 
 |-  ( ph -> sum_ k e. ( M ... ( N + 1 ) ) A = ( sum_ k e. ( M ... ( ( N + 1 ) - 1 ) ) A + B ) )
7 eluzelz 
 |-  ( N e. ( ZZ>= ` M ) -> N e. ZZ )
8 1 7 syl 
 |-  ( ph -> N e. ZZ )
9 8 zcnd 
 |-  ( ph -> N e. CC )
10 1cnd 
 |-  ( ph -> 1 e. CC )
11 9 10 pncand 
 |-  ( ph -> ( ( N + 1 ) - 1 ) = N )
12 11 oveq2d 
 |-  ( ph -> ( M ... ( ( N + 1 ) - 1 ) ) = ( M ... N ) )
13 12 sumeq1d 
 |-  ( ph -> sum_ k e. ( M ... ( ( N + 1 ) - 1 ) ) A = sum_ k e. ( M ... N ) A )
14 13 oveq1d 
 |-  ( ph -> ( sum_ k e. ( M ... ( ( N + 1 ) - 1 ) ) A + B ) = ( sum_ k e. ( M ... N ) A + B ) )
15 6 14 eqtrd 
 |-  ( ph -> sum_ k e. ( M ... ( N + 1 ) ) A = ( sum_ k e. ( M ... N ) A + B ) )