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

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