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

Metamath Proof Explorer

Theorem fzosump1

Description: Separate out the last term in a finite sum. (Contributed by Mario Carneiro, 13-Apr-2016)

Ref Expression
Hypotheses fsumm1.1 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
fsumm1.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐴 ∈ ℂ )
fsumm1.3 ⊢ ( 𝑘 = 𝑁 → 𝐴 = 𝐵 )
Assertion fzosump1 ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ..^ ( 𝑁 + 1 ) ) 𝐴 = ( Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) 𝐴 + 𝐵 ) )

Proof

Step Hyp Ref Expression
1 fsumm1.1 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
2 fsumm1.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐴 ∈ ℂ )
3 fsumm1.3 ⊢ ( 𝑘 = 𝑁 → 𝐴 = 𝐵 )
4 eluzelz ⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑁 ∈ ℤ )
5 1 4 syl ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
6 fzoval ⊢ ( 𝑁 ∈ ℤ → ( 𝑀 ..^ 𝑁 ) = ( 𝑀 ... ( 𝑁 − 1 ) ) )
7 5 6 syl ⊢ ( 𝜑 → ( 𝑀 ..^ 𝑁 ) = ( 𝑀 ... ( 𝑁 − 1 ) ) )
8 7 sumeq1d ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) 𝐴 = Σ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) 𝐴 )
9 8 oveq1d ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) 𝐴 + 𝐵 ) = ( Σ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) 𝐴 + 𝐵 ) )
10 1 2 3 fsumm1 ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴 = ( Σ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) 𝐴 + 𝐵 ) )
11 fzval3 ⊢ ( 𝑁 ∈ ℤ → ( 𝑀 ... 𝑁 ) = ( 𝑀 ..^ ( 𝑁 + 1 ) ) )
12 5 11 syl ⊢ ( 𝜑 → ( 𝑀 ... 𝑁 ) = ( 𝑀 ..^ ( 𝑁 + 1 ) ) )
13 12 sumeq1d ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ... 𝑁 ) 𝐴 = Σ 𝑘 ∈ ( 𝑀 ..^ ( 𝑁 + 1 ) ) 𝐴 )
14 9 10 13 3eqtr2rd ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ..^ ( 𝑁 + 1 ) ) 𝐴 = ( Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) 𝐴 + 𝐵 ) )