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

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