Metamath Proof Explorer

Theorem fzrevral2

Description: Reversal of scanning order inside of a universal quantification restricted to a finite set of sequential integers. (Contributed by NM, 25-Nov-2005)

Ref Expression
Assertion fzrevral2 ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ K ∈ ℤ → ∀ j ∈ K − N … K − M φ ↔ ∀ k ∈ M … N [˙K − k / j]˙ φ

Proof

Step Hyp Ref Expression
1 zsubcl ⊢ K ∈ ℤ ∧ N ∈ ℤ → K − N ∈ ℤ
2 1 3adant2 ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ → K − N ∈ ℤ
3 zsubcl ⊢ K ∈ ℤ ∧ M ∈ ℤ → K − M ∈ ℤ
4 3 3adant3 ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ → K − M ∈ ℤ
5 simp1 ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ → K ∈ ℤ
6 fzrevral ⊢ K − N ∈ ℤ ∧ K − M ∈ ℤ ∧ K ∈ ℤ → ∀ j ∈ K − N … K − M φ ↔ ∀ k ∈ K − K − M … K − K − N [˙K − k / j]˙ φ
7 2 4 5 6 syl3anc ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ → ∀ j ∈ K − N … K − M φ ↔ ∀ k ∈ K − K − M … K − K − N [˙K − k / j]˙ φ
8 zcn ⊢ K ∈ ℤ → K ∈ ℂ
9 zcn ⊢ M ∈ ℤ → M ∈ ℂ
10 zcn ⊢ N ∈ ℤ → N ∈ ℂ
11 nncan ⊢ K ∈ ℂ ∧ M ∈ ℂ → K − K − M = M
12 11 3adant3 ⊢ K ∈ ℂ ∧ M ∈ ℂ ∧ N ∈ ℂ → K − K − M = M
13 nncan ⊢ K ∈ ℂ ∧ N ∈ ℂ → K − K − N = N
14 13 3adant2 ⊢ K ∈ ℂ ∧ M ∈ ℂ ∧ N ∈ ℂ → K − K − N = N
15 12 14 oveq12d ⊢ K ∈ ℂ ∧ M ∈ ℂ ∧ N ∈ ℂ → K − K − M … K − K − N = M … N
16 8 9 10 15 syl3an ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ → K − K − M … K − K − N = M … N
17 16 raleqdv ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ → ∀ k ∈ K − K − M … K − K − N [˙K − k / j]˙ φ ↔ ∀ k ∈ M … N [˙K − k / j]˙ φ
18 7 17 bitrd ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ → ∀ j ∈ K − N … K − M φ ↔ ∀ k ∈ M … N [˙K − k / j]˙ φ
19 18 3coml ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ K ∈ ℤ → ∀ j ∈ K − N … K − M φ ↔ ∀ k ∈ M … N [˙K − k / j]˙ φ