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 ... 𝑁 ) 𝐴 + 𝐵 ) )