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

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 ⊢ ( 𝜑 → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
fzosumm1.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝐴 ∈ ℂ )
fzosumm1.3 ⊢ ( 𝑘 = ( 𝑁 − 1 ) → 𝐴 = 𝐵 )
fzosumm1.n ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
Assertion fzosumm1 ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) 𝐴 = ( Σ 𝑘 ∈ ( 𝑀 ..^ ( 𝑁 − 1 ) ) 𝐴 + 𝐵 ) )

Proof

Step Hyp Ref Expression
1 fzosumm1.1 ⊢ ( 𝜑 → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
2 fzosumm1.2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) → 𝐴 ∈ ℂ )
3 fzosumm1.3 ⊢ ( 𝑘 = ( 𝑁 − 1 ) → 𝐴 = 𝐵 )
4 fzosumm1.n ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
5 fzoval ⊢ ( 𝑁 ∈ ℤ → ( 𝑀 ..^ 𝑁 ) = ( 𝑀 ... ( 𝑁 − 1 ) ) )
6 4 5 syl ⊢ ( 𝜑 → ( 𝑀 ..^ 𝑁 ) = ( 𝑀 ... ( 𝑁 − 1 ) ) )
7 6 eqcomd ⊢ ( 𝜑 → ( 𝑀 ... ( 𝑁 − 1 ) ) = ( 𝑀 ..^ 𝑁 ) )
8 7 eleq2d ⊢ ( 𝜑 → ( 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ↔ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) ) )
9 8 biimpa ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) )
10 9 2 syldan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → 𝐴 ∈ ℂ )
11 1 10 3 fsumm1 ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) 𝐴 = ( Σ 𝑘 ∈ ( 𝑀 ... ( ( 𝑁 − 1 ) − 1 ) ) 𝐴 + 𝐵 ) )
12 6 sumeq1d ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) 𝐴 = Σ 𝑘 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) 𝐴 )
13 eluzelz ⊢ ( ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑁 − 1 ) ∈ ℤ )
14 fzoval ⊢ ( ( 𝑁 − 1 ) ∈ ℤ → ( 𝑀 ..^ ( 𝑁 − 1 ) ) = ( 𝑀 ... ( ( 𝑁 − 1 ) − 1 ) ) )
15 1 13 14 3syl ⊢ ( 𝜑 → ( 𝑀 ..^ ( 𝑁 − 1 ) ) = ( 𝑀 ... ( ( 𝑁 − 1 ) − 1 ) ) )
16 15 sumeq1d ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ..^ ( 𝑁 − 1 ) ) 𝐴 = Σ 𝑘 ∈ ( 𝑀 ... ( ( 𝑁 − 1 ) − 1 ) ) 𝐴 )
17 16 oveq1d ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( 𝑀 ..^ ( 𝑁 − 1 ) ) 𝐴 + 𝐵 ) = ( Σ 𝑘 ∈ ( 𝑀 ... ( ( 𝑁 − 1 ) − 1 ) ) 𝐴 + 𝐵 ) )
18 11 12 17 3eqtr4d ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ..^ 𝑁 ) 𝐴 = ( Σ 𝑘 ∈ ( 𝑀 ..^ ( 𝑁 − 1 ) ) 𝐴 + 𝐵 ) )