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

Metamath Proof Explorer

Theorem fsumshft

Description: Index shift of a finite sum. (Contributed by NM, 27-Nov-2005) (Revised by Mario Carneiro, 24-Apr-2014) (Proof shortened by AV, 8-Sep-2019)

Ref Expression
Hypotheses fsumrev.1 ⊢ φ → K ∈ ℤ
fsumrev.2 ⊢ φ → M ∈ ℤ
fsumrev.3 ⊢ φ → N ∈ ℤ
fsumrev.4 ⊢ φ ∧ j ∈ M … N → A ∈ ℂ
fsumshft.5 ⊢ j = k − K → A = B
Assertion fsumshft ⊢ φ → ∑ 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 fsumshft.5 ⊢ j = k − K → A = B
6 fzfid ⊢ φ → M + K … N + K ∈ Fin
7 1 2 3 mptfzshft ⊢ φ → j ∈ M + K … N + K ⟼ j − K : M + K … N + K ⟶ 1-1 onto M … N
8 oveq1 ⊢ j = k → j − K = k − K
9 eqid ⊢ j ∈ M + K … N + K ⟼ j − K = j ∈ M + K … N + K ⟼ j − K
10 ovex ⊢ k − K ∈ V
11 8 9 10 fvmpt ⊢ k ∈ M + K … N + K → j ∈ M + K … N + K ⟼ j − K ⁡ k = k − K
12 11 adantl ⊢ φ ∧ k ∈ M + K … N + K → j ∈ M + K … N + K ⟼ j − K ⁡ k = k − K
13 5 6 7 12 4 fsumf1o ⊢ φ → ∑ j = M N A = ∑ k = M + K N + K B