Metamath Proof Explorer

Theorem fzosumm1

Description: Separate out the last term in a finite sum. (Contributed by Steven Nguyen, 22-Aug-2023)

Ref Expression
Hypotheses fzosumm1.1 ⊢ φ → N − 1 ∈ ℤ ≥ M
fzosumm1.2 ⊢ φ ∧ k ∈ M ..^ N → A ∈ ℂ
fzosumm1.3 ⊢ k = N − 1 → A = B
fzosumm1.n ⊢ φ → N ∈ ℤ
Assertion fzosumm1 ⊢ φ → ∑ k ∈ M ..^ N A = ∑ k ∈ M ..^ N − 1 A + B

Proof

Step Hyp Ref Expression
1 fzosumm1.1 ⊢ φ → N − 1 ∈ ℤ ≥ M
2 fzosumm1.2 ⊢ φ ∧ k ∈ M ..^ N → A ∈ ℂ
3 fzosumm1.3 ⊢ k = N − 1 → A = B
4 fzosumm1.n ⊢ φ → N ∈ ℤ
5 fzoval ⊢ N ∈ ℤ → M ..^ N = M … N − 1
6 4 5 syl ⊢ φ → M ..^ N = M … N − 1
7 6 eqcomd ⊢ φ → M … N − 1 = M ..^ N
8 7 eleq2d ⊢ φ → k ∈ M … N − 1 ↔ k ∈ M ..^ N
9 8 biimpa ⊢ φ ∧ k ∈ M … N − 1 → k ∈ M ..^ N
10 9 2 syldan ⊢ φ ∧ k ∈ M … N − 1 → A ∈ ℂ
11 1 10 3 fsumm1 ⊢ φ → ∑ k = M N − 1 A = ∑ k = M N - 1 - 1 A + B
12 6 sumeq1d ⊢ φ → ∑ k ∈ M ..^ N A = ∑ k = M N − 1 A
13 eluzelz ⊢ N − 1 ∈ ℤ ≥ M → N − 1 ∈ ℤ
14 fzoval ⊢ N − 1 ∈ ℤ → M ..^ N − 1 = M … N - 1 - 1
15 1 13 14 3syl ⊢ φ → M ..^ N − 1 = M … N - 1 - 1
16 15 sumeq1d ⊢ φ → ∑ k ∈ M ..^ N − 1 A = ∑ k = M N - 1 - 1 A
17 16 oveq1d ⊢ φ → ∑ k ∈ M ..^ N − 1 A + B = ∑ k = M N - 1 - 1 A + B
18 11 12 17 3eqtr4d ⊢ φ → ∑ k ∈ M ..^ N A = ∑ k ∈ M ..^ N − 1 A + B