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

Metamath Proof Explorer

Theorem fsumshftd

Description: Index shift of a finite sum with a weaker "implicit substitution" hypothesis than fsumshft . The proof demonstrates how this can be derived starting from from fsumshft . (Contributed by NM, 1-Nov-2019)

Ref Expression
Hypotheses fsumshftd.1 ⊢ φ → K ∈ ℤ
fsumshftd.2 ⊢ φ → M ∈ ℤ
fsumshftd.3 ⊢ φ → N ∈ ℤ
fsumshftd.4 ⊢ φ ∧ j ∈ M … N → A ∈ ℂ
fsumshftd.5 ⊢ φ ∧ j = k − K → A = B
Assertion fsumshftd ⊢ φ → ∑ j = M N A = ∑ k = M + K N + K B

Proof

Step Hyp Ref Expression
1 fsumshftd.1 ⊢ φ → K ∈ ℤ
2 fsumshftd.2 ⊢ φ → M ∈ ℤ
3 fsumshftd.3 ⊢ φ → N ∈ ℤ
4 fsumshftd.4 ⊢ φ ∧ j ∈ M … N → A ∈ ℂ
5 fsumshftd.5 ⊢ φ ∧ j = k − K → A = B
6 csbeq1a ⊢ j = w → A = ⦋ w / j⦌ A
7 nfcv ⊢ Ⅎ _ w A
8 nfcsb1v ⊢ Ⅎ _ j ⦋ w / j⦌ A
9 6 7 8 cbvsum ⊢ ∑ j = M N A = ∑ w = M N ⦋ w / j⦌ A
10 nfv ⊢ Ⅎ j φ ∧ w ∈ M … N
11 8 nfel1 ⊢ Ⅎ j ⦋ w / j⦌ A ∈ ℂ
12 10 11 nfim ⊢ Ⅎ j φ ∧ w ∈ M … N → ⦋ w / j⦌ A ∈ ℂ
13 eleq1w ⊢ j = w → j ∈ M … N ↔ w ∈ M … N
14 13 anbi2d ⊢ j = w → φ ∧ j ∈ M … N ↔ φ ∧ w ∈ M … N
15 6 eleq1d ⊢ j = w → A ∈ ℂ ↔ ⦋ w / j⦌ A ∈ ℂ
16 14 15 imbi12d ⊢ j = w → φ ∧ j ∈ M … N → A ∈ ℂ ↔ φ ∧ w ∈ M … N → ⦋ w / j⦌ A ∈ ℂ
17 12 16 4 chvarfv ⊢ φ ∧ w ∈ M … N → ⦋ w / j⦌ A ∈ ℂ
18 csbeq1 ⊢ w = k − K → ⦋ w / j⦌ A = ⦋ k − K / j⦌ A
19 1 2 3 17 18 fsumshft ⊢ φ → ∑ w = M N ⦋ w / j⦌ A = ∑ k = M + K N + K ⦋ k − K / j⦌ A
20 ovexd ⊢ φ → k − K ∈ V
21 20 5 csbied ⊢ φ → ⦋ k − K / j⦌ A = B
22 21 sumeq2sdv ⊢ φ → ∑ k = M + K N + K ⦋ k − K / j⦌ A = ∑ k = M + K N + K B
23 19 22 eqtrd ⊢ φ → ∑ w = M N ⦋ w / j⦌ A = ∑ k = M + K N + K B
24 9 23 eqtrid ⊢ φ → ∑ j = M N A = ∑ k = M + K N + K B