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

Metamath Proof Explorer

Theorem fsumshftm

Description: Negative index shift of a finite sum. (Contributed by NM, 28-Nov-2005) (Revised by Mario Carneiro, 24-Apr-2014)

Ref Expression
Hypotheses fsumrev.1 ⊢ ( 𝜑 → 𝐾 ∈ ℤ )
fsumrev.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
fsumrev.3 ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
fsumrev.4 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐴 ∈ ℂ )
fsumshftm.5 ⊢ ( 𝑗 = ( 𝑘 + 𝐾 ) → 𝐴 = 𝐵 )
Assertion fsumshftm ( 𝜑 → Σ 𝑗 ∈ ( 𝑀 ... 𝑁 ) 𝐴 = Σ 𝑘 ∈ ( ( 𝑀 − 𝐾 ) ... ( 𝑁 − 𝐾 ) ) 𝐵 )

Proof

Step Hyp Ref Expression
1 fsumrev.1 ⊢ ( 𝜑 → 𝐾 ∈ ℤ )
2 fsumrev.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 fsumrev.3 ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
4 fsumrev.4 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐴 ∈ ℂ )
5 fsumshftm.5 ⊢ ( 𝑗 = ( 𝑘 + 𝐾 ) → 𝐴 = 𝐵 )
6 csbeq1a ⊢ ( 𝑗 = 𝑚 → 𝐴 = ⦋ 𝑚 / 𝑗 ⦌ 𝐴 )
7 nfcv ⊢ Ⅎ 𝑚 𝐴
8 nfcsb1v ⊢ Ⅎ 𝑗 ⦋ 𝑚 / 𝑗 ⦌ 𝐴
9 6 7 8 cbvsum ⊢ Σ 𝑗 ∈ ( 𝑀 ... 𝑁 ) 𝐴 = Σ 𝑚 ∈ ( 𝑀 ... 𝑁 ) ⦋ 𝑚 / 𝑗 ⦌ 𝐴
10 1 znegcld ⊢ ( 𝜑 → - 𝐾 ∈ ℤ )
11 4 ralrimiva ⊢ ( 𝜑 → ∀ 𝑗 ∈ ( 𝑀 ... 𝑁 ) 𝐴 ∈ ℂ )
12 8 nfel1 ⊢ Ⅎ 𝑗 ⦋ 𝑚 / 𝑗 ⦌ 𝐴 ∈ ℂ
13 6 eleq1d ⊢ ( 𝑗 = 𝑚 → ( 𝐴 ∈ ℂ ↔ ⦋ 𝑚 / 𝑗 ⦌ 𝐴 ∈ ℂ ) )
14 12 13 rspc ⊢ ( 𝑚 ∈ ( 𝑀 ... 𝑁 ) → ( ∀ 𝑗 ∈ ( 𝑀 ... 𝑁 ) 𝐴 ∈ ℂ → ⦋ 𝑚 / 𝑗 ⦌ 𝐴 ∈ ℂ ) )
15 11 14 mpan9 ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( 𝑀 ... 𝑁 ) ) → ⦋ 𝑚 / 𝑗 ⦌ 𝐴 ∈ ℂ )
16 csbeq1 ⊢ ( 𝑚 = ( 𝑘 − - 𝐾 ) → ⦋ 𝑚 / 𝑗 ⦌ 𝐴 = ⦋ ( 𝑘 − - 𝐾 ) / 𝑗 ⦌ 𝐴 )
17 10 2 3 15 16 fsumshft ⊢ ( 𝜑 → Σ 𝑚 ∈ ( 𝑀 ... 𝑁 ) ⦋ 𝑚 / 𝑗 ⦌ 𝐴 = Σ 𝑘 ∈ ( ( 𝑀 + - 𝐾 ) ... ( 𝑁 + - 𝐾 ) ) ⦋ ( 𝑘 − - 𝐾 ) / 𝑗 ⦌ 𝐴 )
18 2 zcnd ⊢ ( 𝜑 → 𝑀 ∈ ℂ )
19 1 zcnd ⊢ ( 𝜑 → 𝐾 ∈ ℂ )
20 18 19 negsubd ⊢ ( 𝜑 → ( 𝑀 + - 𝐾 ) = ( 𝑀 − 𝐾 ) )
21 3 zcnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
22 21 19 negsubd ⊢ ( 𝜑 → ( 𝑁 + - 𝐾 ) = ( 𝑁 − 𝐾 ) )
23 20 22 oveq12d ⊢ ( 𝜑 → ( ( 𝑀 + - 𝐾 ) ... ( 𝑁 + - 𝐾 ) ) = ( ( 𝑀 − 𝐾 ) ... ( 𝑁 − 𝐾 ) ) )
24 23 sumeq1d ⊢ ( 𝜑 → Σ 𝑘 ∈ ( ( 𝑀 + - 𝐾 ) ... ( 𝑁 + - 𝐾 ) ) ⦋ ( 𝑘 − - 𝐾 ) / 𝑗 ⦌ 𝐴 = Σ 𝑘 ∈ ( ( 𝑀 − 𝐾 ) ... ( 𝑁 − 𝐾 ) ) ⦋ ( 𝑘 − - 𝐾 ) / 𝑗 ⦌ 𝐴 )
25 elfzelz ⊢ ( 𝑘 ∈ ( ( 𝑀 − 𝐾 ) ... ( 𝑁 − 𝐾 ) ) → 𝑘 ∈ ℤ )
26 25 zcnd ⊢ ( 𝑘 ∈ ( ( 𝑀 − 𝐾 ) ... ( 𝑁 − 𝐾 ) ) → 𝑘 ∈ ℂ )
27 subneg ⊢ ( ( 𝑘 ∈ ℂ ∧ 𝐾 ∈ ℂ ) → ( 𝑘 − - 𝐾 ) = ( 𝑘 + 𝐾 ) )
28 26 19 27 syl2anr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 − 𝐾 ) ... ( 𝑁 − 𝐾 ) ) ) → ( 𝑘 − - 𝐾 ) = ( 𝑘 + 𝐾 ) )
29 28 csbeq1d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 − 𝐾 ) ... ( 𝑁 − 𝐾 ) ) ) → ⦋ ( 𝑘 − - 𝐾 ) / 𝑗 ⦌ 𝐴 = ⦋ ( 𝑘 + 𝐾 ) / 𝑗 ⦌ 𝐴 )
30 ovex ⊢ ( 𝑘 + 𝐾 ) ∈ V
31 30 5 csbie ⊢ ⦋ ( 𝑘 + 𝐾 ) / 𝑗 ⦌ 𝐴 = 𝐵
32 29 31 eqtrdi ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 𝑀 − 𝐾 ) ... ( 𝑁 − 𝐾 ) ) ) → ⦋ ( 𝑘 − - 𝐾 ) / 𝑗 ⦌ 𝐴 = 𝐵 )
33 32 sumeq2dv ⊢ ( 𝜑 → Σ 𝑘 ∈ ( ( 𝑀 − 𝐾 ) ... ( 𝑁 − 𝐾 ) ) ⦋ ( 𝑘 − - 𝐾 ) / 𝑗 ⦌ 𝐴 = Σ 𝑘 ∈ ( ( 𝑀 − 𝐾 ) ... ( 𝑁 − 𝐾 ) ) 𝐵 )
34 17 24 33 3eqtrd ⊢ ( 𝜑 → Σ 𝑚 ∈ ( 𝑀 ... 𝑁 ) ⦋ 𝑚 / 𝑗 ⦌ 𝐴 = Σ 𝑘 ∈ ( ( 𝑀 − 𝐾 ) ... ( 𝑁 − 𝐾 ) ) 𝐵 )
35 9 34 eqtrid ⊢ ( 𝜑 → Σ 𝑗 ∈ ( 𝑀 ... 𝑁 ) 𝐴 = Σ 𝑘 ∈ ( ( 𝑀 − 𝐾 ) ... ( 𝑁 − 𝐾 ) ) 𝐵 )