Metamath Proof Explorer

Theorem fz1sump1

Description: Add one more term to a sum. Special case of fsump1 generalized to N e. NN0 . (Contributed by SN, 22-Mar-2025)

Ref Expression
Hypotheses fz1sump1.n 
|- ( ph -> N e. NN0 )
fz1sump1.a 
|- ( ( ph /\ k e. ( 1 ... ( N + 1 ) ) ) -> A e. CC )
fz1sump1.s 
|- ( k = ( N + 1 ) -> A = B )
Assertion fz1sump1 
|- ( ph -> sum_ k e. ( 1 ... ( N + 1 ) ) A = ( sum_ k e. ( 1 ... N ) A + B ) )

Proof

Step Hyp Ref Expression
1 fz1sump1.n 
 |-  ( ph -> N e. NN0 )
2 fz1sump1.a 
 |-  ( ( ph /\ k e. ( 1 ... ( N + 1 ) ) ) -> A e. CC )
3 fz1sump1.s 
 |-  ( k = ( N + 1 ) -> A = B )
4 nn0p1nn 
 |-  ( N e. NN0 -> ( N + 1 ) e. NN )
5 1 4 syl 
 |-  ( ph -> ( N + 1 ) e. NN )
6 nnuz 
 |-  NN = ( ZZ>= ` 1 )
7 5 6 eleqtrdi 
 |-  ( ph -> ( N + 1 ) e. ( ZZ>= ` 1 ) )
8 7 2 3 fsumm1 
 |-  ( ph -> sum_ k e. ( 1 ... ( N + 1 ) ) A = ( sum_ k e. ( 1 ... ( ( N + 1 ) - 1 ) ) A + B ) )
9 1 nn0cnd 
 |-  ( ph -> N e. CC )
10 1cnd 
 |-  ( ph -> 1 e. CC )
11 9 10 pncand 
 |-  ( ph -> ( ( N + 1 ) - 1 ) = N )
12 11 oveq2d 
 |-  ( ph -> ( 1 ... ( ( N + 1 ) - 1 ) ) = ( 1 ... N ) )
13 12 sumeq1d 
 |-  ( ph -> sum_ k e. ( 1 ... ( ( N + 1 ) - 1 ) ) A = sum_ k e. ( 1 ... N ) A )
14 13 oveq1d 
 |-  ( ph -> ( sum_ k e. ( 1 ... ( ( N + 1 ) - 1 ) ) A + B ) = ( sum_ k e. ( 1 ... N ) A + B ) )
15 8 14 eqtrd 
 |-  ( ph -> sum_ k e. ( 1 ... ( N + 1 ) ) A = ( sum_ k e. ( 1 ... N ) A + B ) )