# Metamath Proof Explorer

## Theorem fprodshft

Description: Shift the index of a finite product. (Contributed by Scott Fenton, 5-Jan-2018)

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

### Proof

Step Hyp Ref Expression
1 fprodshft.1 $⊢ φ → K ∈ ℤ$
2 fprodshft.2 $⊢ φ → M ∈ ℤ$
3 fprodshft.3 $⊢ φ → N ∈ ℤ$
4 fprodshft.4 $⊢ φ ∧ j ∈ M … N → A ∈ ℂ$
5 fprodshft.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 fprodf1o $⊢ φ → ∏ j = M N A = ∏ k = M + K N + K B$