Metamath Proof Explorer

Theorem fzoshftral

Description: Shift the scanning order inside of a universal quantification restricted to a half-open integer range, analogous to fzshftral . (Contributed by Alexander van der Vekens, 23-Sep-2018)

Ref Expression
Assertion fzoshftral ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ K ∈ ℤ → ∀ j ∈ M ..^ N φ ↔ ∀ k ∈ M + K ..^ N + K [˙k − K / j]˙ φ

Proof

Step Hyp Ref Expression
1 fzoval ⊢ N ∈ ℤ → M ..^ N = M … N − 1
2 1 3ad2ant2 ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ K ∈ ℤ → M ..^ N = M … N − 1
3 2 raleqdv ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ K ∈ ℤ → ∀ j ∈ M ..^ N φ ↔ ∀ j ∈ M … N − 1 φ
4 peano2zm ⊢ N ∈ ℤ → N − 1 ∈ ℤ
5 fzshftral ⊢ M ∈ ℤ ∧ N − 1 ∈ ℤ ∧ K ∈ ℤ → ∀ j ∈ M … N − 1 φ ↔ ∀ k ∈ M + K … N - 1 + K [˙k − K / j]˙ φ
6 4 5 syl3an2 ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ K ∈ ℤ → ∀ j ∈ M … N − 1 φ ↔ ∀ k ∈ M + K … N - 1 + K [˙k − K / j]˙ φ
7 zaddcl ⊢ N ∈ ℤ ∧ K ∈ ℤ → N + K ∈ ℤ
8 7 3adant1 ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ K ∈ ℤ → N + K ∈ ℤ
9 fzoval ⊢ N + K ∈ ℤ → M + K ..^ N + K = M + K … N + K - 1
10 8 9 syl ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ K ∈ ℤ → M + K ..^ N + K = M + K … N + K - 1
11 zcn ⊢ N ∈ ℤ → N ∈ ℂ
12 11 adantr ⊢ N ∈ ℤ ∧ K ∈ ℤ → N ∈ ℂ
13 zcn ⊢ K ∈ ℤ → K ∈ ℂ
14 13 adantl ⊢ N ∈ ℤ ∧ K ∈ ℤ → K ∈ ℂ
15 1cnd ⊢ N ∈ ℤ ∧ K ∈ ℤ → 1 ∈ ℂ
16 12 14 15 addsubd ⊢ N ∈ ℤ ∧ K ∈ ℤ → N + K - 1 = N - 1 + K
17 16 3adant1 ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ K ∈ ℤ → N + K - 1 = N - 1 + K
18 17 oveq2d ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ K ∈ ℤ → M + K … N + K - 1 = M + K … N - 1 + K
19 10 18 eqtr2d ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ K ∈ ℤ → M + K … N - 1 + K = M + K ..^ N + K
20 19 raleqdv ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ K ∈ ℤ → ∀ k ∈ M + K … N - 1 + K [˙k − K / j]˙ φ ↔ ∀ k ∈ M + K ..^ N + K [˙k − K / j]˙ φ
21 3 6 20 3bitrd ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ K ∈ ℤ → ∀ j ∈ M ..^ N φ ↔ ∀ k ∈ M + K ..^ N + K [˙k − K / j]˙ φ