# 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 $⊢ φ → K ∈ ℤ$
fsumrev.2 $⊢ φ → M ∈ ℤ$
fsumrev.3 $⊢ φ → N ∈ ℤ$
fsumrev.4 $⊢ φ ∧ j ∈ M … N → A ∈ ℂ$
fsumshftm.5 $⊢ j = k + K → A = B$
Assertion fsumshftm $⊢ φ → ∑ j = M N A = ∑ k = M − K N − K B$

### Proof

Step Hyp Ref Expression
1 fsumrev.1 $⊢ φ → K ∈ ℤ$
2 fsumrev.2 $⊢ φ → M ∈ ℤ$
3 fsumrev.3 $⊢ φ → N ∈ ℤ$
4 fsumrev.4 $⊢ φ ∧ j ∈ M … N → A ∈ ℂ$
5 fsumshftm.5 $⊢ j = k + K → A = B$
6 nfcv $⊢ Ⅎ _ m A$
7 nfcsb1v
8 csbeq1a
9 6 7 8 cbvsumi
10 1 znegcld $⊢ φ → − K ∈ ℤ$
11 4 ralrimiva $⊢ φ → ∀ j ∈ M … N A ∈ ℂ$
12 7 nfel1
13 8 eleq1d
14 12 13 rspc
15 11 14 mpan9
16 csbeq1
17 10 2 3 15 16 fsumshft
18 2 zcnd $⊢ φ → M ∈ ℂ$
19 1 zcnd $⊢ φ → K ∈ ℂ$
20 18 19 negsubd $⊢ φ → M + − K = M − K$
21 3 zcnd $⊢ φ → N ∈ ℂ$
22 21 19 negsubd $⊢ φ → N + − K = N − K$
23 20 22 oveq12d $⊢ φ → M + − K … N + − K = M − K … N − K$
24 23 sumeq1d
25 elfzelz $⊢ k ∈ M − K … N − K → k ∈ ℤ$
26 25 zcnd $⊢ k ∈ M − K … N − K → k ∈ ℂ$
27 subneg $⊢ k ∈ ℂ ∧ K ∈ ℂ → k − − K = k + K$
28 26 19 27 syl2anr $⊢ φ ∧ k ∈ M − K … N − K → k − − K = k + K$
29 28 csbeq1d
30 ovex $⊢ k + K ∈ V$
31 30 5 csbie
32 29 31 eqtrdi
33 32 sumeq2dv
34 17 24 33 3eqtrd
35 9 34 syl5eq $⊢ φ → ∑ j = M N A = ∑ k = M − K N − K B$