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 φ N 0
fz1sump1.a φ k 1 N + 1 A
fz1sump1.s k = N + 1 A = B
Assertion fz1sump1 φ k = 1 N + 1 A = k = 1 N A + B

Proof

Step Hyp Ref Expression
1 fz1sump1.n φ N 0
2 fz1sump1.a φ k 1 N + 1 A
3 fz1sump1.s k = N + 1 A = B
4 nn0p1nn N 0 N + 1
5 1 4 syl φ N + 1
6 nnuz = 1
7 5 6 eleqtrdi φ N + 1 1
8 7 2 3 fsumm1 φ k = 1 N + 1 A = k = 1 N + 1 - 1 A + B
9 1 nn0cnd φ N
10 1cnd φ 1
11 9 10 pncand φ N + 1 - 1 = N
12 11 oveq2d φ 1 N + 1 - 1 = 1 N
13 12 sumeq1d φ k = 1 N + 1 - 1 A = k = 1 N A
14 13 oveq1d φ k = 1 N + 1 - 1 A + B = k = 1 N A + B
15 8 14 eqtrd φ k = 1 N + 1 A = k = 1 N A + B