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 ( 𝜑𝑁 ∈ ℕ0 )
fz1sump1.a ( ( 𝜑𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → 𝐴 ∈ ℂ )
fz1sump1.s ( 𝑘 = ( 𝑁 + 1 ) → 𝐴 = 𝐵 )
Assertion fz1sump1 ( 𝜑 → Σ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) 𝐴 = ( Σ 𝑘 ∈ ( 1 ... 𝑁 ) 𝐴 + 𝐵 ) )

Proof

Step Hyp Ref Expression
1 fz1sump1.n ( 𝜑𝑁 ∈ ℕ0 )
2 fz1sump1.a ( ( 𝜑𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) ) → 𝐴 ∈ ℂ )
3 fz1sump1.s ( 𝑘 = ( 𝑁 + 1 ) → 𝐴 = 𝐵 )
4 nn0p1nn ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ )
5 1 4 syl ( 𝜑 → ( 𝑁 + 1 ) ∈ ℕ )
6 nnuz ℕ = ( ℤ ‘ 1 )
7 5 6 eleqtrdi ( 𝜑 → ( 𝑁 + 1 ) ∈ ( ℤ ‘ 1 ) )
8 7 2 3 fsumm1 ( 𝜑 → Σ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) 𝐴 = ( Σ 𝑘 ∈ ( 1 ... ( ( 𝑁 + 1 ) − 1 ) ) 𝐴 + 𝐵 ) )
9 1 nn0cnd ( 𝜑𝑁 ∈ ℂ )
10 1cnd ( 𝜑 → 1 ∈ ℂ )
11 9 10 pncand ( 𝜑 → ( ( 𝑁 + 1 ) − 1 ) = 𝑁 )
12 11 oveq2d ( 𝜑 → ( 1 ... ( ( 𝑁 + 1 ) − 1 ) ) = ( 1 ... 𝑁 ) )
13 12 sumeq1d ( 𝜑 → Σ 𝑘 ∈ ( 1 ... ( ( 𝑁 + 1 ) − 1 ) ) 𝐴 = Σ 𝑘 ∈ ( 1 ... 𝑁 ) 𝐴 )
14 13 oveq1d ( 𝜑 → ( Σ 𝑘 ∈ ( 1 ... ( ( 𝑁 + 1 ) − 1 ) ) 𝐴 + 𝐵 ) = ( Σ 𝑘 ∈ ( 1 ... 𝑁 ) 𝐴 + 𝐵 ) )
15 8 14 eqtrd ( 𝜑 → Σ 𝑘 ∈ ( 1 ... ( 𝑁 + 1 ) ) 𝐴 = ( Σ 𝑘 ∈ ( 1 ... 𝑁 ) 𝐴 + 𝐵 ) )