Metamath Proof Explorer

Theorem fzrevral

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 fzrevral ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ∀ 𝑗 ∈ ( 𝑀 ... 𝑁 ) 𝜑 ↔ ∀ 𝑘 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) [ ( 𝐾 − 𝑘 ) / 𝑗 ] 𝜑 ) )

Proof

Step Hyp Ref Expression
1 simpr ⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 ∈ ℤ ) ∧ 𝑘 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ) → 𝑘 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) )
2 elfzelz ⊢ ( 𝑘 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) → 𝑘 ∈ ℤ )
3 fzrev ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐾 ∈ ℤ ∧ 𝑘 ∈ ℤ ) ) → ( 𝑘 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ↔ ( 𝐾 − 𝑘 ) ∈ ( 𝑀 ... 𝑁 ) ) )
4 3 anassrs ⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 ∈ ℤ ) ∧ 𝑘 ∈ ℤ ) → ( 𝑘 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ↔ ( 𝐾 − 𝑘 ) ∈ ( 𝑀 ... 𝑁 ) ) )
5 2 4 sylan2 ⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 ∈ ℤ ) ∧ 𝑘 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ) → ( 𝑘 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ↔ ( 𝐾 − 𝑘 ) ∈ ( 𝑀 ... 𝑁 ) ) )
6 1 5 mpbid ⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 ∈ ℤ ) ∧ 𝑘 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ) → ( 𝐾 − 𝑘 ) ∈ ( 𝑀 ... 𝑁 ) )
7 rspsbc ⊢ ( ( 𝐾 − 𝑘 ) ∈ ( 𝑀 ... 𝑁 ) → ( ∀ 𝑗 ∈ ( 𝑀 ... 𝑁 ) 𝜑 → [ ( 𝐾 − 𝑘 ) / 𝑗 ] 𝜑 ) )
8 6 7 syl ⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝐾 ∈ ℤ ) ∧ 𝑘 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) ) → ( ∀ 𝑗 ∈ ( 𝑀 ... 𝑁 ) 𝜑 → [ ( 𝐾 − 𝑘 ) / 𝑗 ] 𝜑 ) )
9 8 ex3 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑘 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) → ( ∀ 𝑗 ∈ ( 𝑀 ... 𝑁 ) 𝜑 → [ ( 𝐾 − 𝑘 ) / 𝑗 ] 𝜑 ) ) )
10 9 com23 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ∀ 𝑗 ∈ ( 𝑀 ... 𝑁 ) 𝜑 → ( 𝑘 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) → [ ( 𝐾 − 𝑘 ) / 𝑗 ] 𝜑 ) ) )
11 10 ralrimdv ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ∀ 𝑗 ∈ ( 𝑀 ... 𝑁 ) 𝜑 → ∀ 𝑘 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) [ ( 𝐾 − 𝑘 ) / 𝑗 ] 𝜑 ) )
12 nfv ⊢ Ⅎ 𝑗 𝐾 ∈ ℤ
13 nfcv ⊢ Ⅎ 𝑗 ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) )
14 nfsbc1v ⊢ Ⅎ 𝑗 [ ( 𝐾 − 𝑘 ) / 𝑗 ] 𝜑
15 13 14 nfralw ⊢ Ⅎ 𝑗 ∀ 𝑘 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) [ ( 𝐾 − 𝑘 ) / 𝑗 ] 𝜑
16 fzrev2i ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑗 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐾 − 𝑗 ) ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) )
17 oveq2 ⊢ ( 𝑘 = ( 𝐾 − 𝑗 ) → ( 𝐾 − 𝑘 ) = ( 𝐾 − ( 𝐾 − 𝑗 ) ) )
18 17 sbceq1d ⊢ ( 𝑘 = ( 𝐾 − 𝑗 ) → ( [ ( 𝐾 − 𝑘 ) / 𝑗 ] 𝜑 ↔ [ ( 𝐾 − ( 𝐾 − 𝑗 ) ) / 𝑗 ] 𝜑 ) )
19 18 rspcv ⊢ ( ( 𝐾 − 𝑗 ) ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) → ( ∀ 𝑘 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) [ ( 𝐾 − 𝑘 ) / 𝑗 ] 𝜑 → [ ( 𝐾 − ( 𝐾 − 𝑗 ) ) / 𝑗 ] 𝜑 ) )
20 16 19 syl ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑗 ∈ ( 𝑀 ... 𝑁 ) ) → ( ∀ 𝑘 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) [ ( 𝐾 − 𝑘 ) / 𝑗 ] 𝜑 → [ ( 𝐾 − ( 𝐾 − 𝑗 ) ) / 𝑗 ] 𝜑 ) )
21 zcn ⊢ ( 𝐾 ∈ ℤ → 𝐾 ∈ ℂ )
22 elfzelz ⊢ ( 𝑗 ∈ ( 𝑀 ... 𝑁 ) → 𝑗 ∈ ℤ )
23 22 zcnd ⊢ ( 𝑗 ∈ ( 𝑀 ... 𝑁 ) → 𝑗 ∈ ℂ )
24 nncan ⊢ ( ( 𝐾 ∈ ℂ ∧ 𝑗 ∈ ℂ ) → ( 𝐾 − ( 𝐾 − 𝑗 ) ) = 𝑗 )
25 21 23 24 syl2an ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑗 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝐾 − ( 𝐾 − 𝑗 ) ) = 𝑗 )
26 25 eqcomd ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑗 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑗 = ( 𝐾 − ( 𝐾 − 𝑗 ) ) )
27 sbceq1a ⊢ ( 𝑗 = ( 𝐾 − ( 𝐾 − 𝑗 ) ) → ( 𝜑 ↔ [ ( 𝐾 − ( 𝐾 − 𝑗 ) ) / 𝑗 ] 𝜑 ) )
28 26 27 syl ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑗 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝜑 ↔ [ ( 𝐾 − ( 𝐾 − 𝑗 ) ) / 𝑗 ] 𝜑 ) )
29 20 28 sylibrd ⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑗 ∈ ( 𝑀 ... 𝑁 ) ) → ( ∀ 𝑘 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) [ ( 𝐾 − 𝑘 ) / 𝑗 ] 𝜑 → 𝜑 ) )
30 29 ex ⊢ ( 𝐾 ∈ ℤ → ( 𝑗 ∈ ( 𝑀 ... 𝑁 ) → ( ∀ 𝑘 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) [ ( 𝐾 − 𝑘 ) / 𝑗 ] 𝜑 → 𝜑 ) ) )
31 30 com23 ⊢ ( 𝐾 ∈ ℤ → ( ∀ 𝑘 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) [ ( 𝐾 − 𝑘 ) / 𝑗 ] 𝜑 → ( 𝑗 ∈ ( 𝑀 ... 𝑁 ) → 𝜑 ) ) )
32 12 15 31 ralrimd ⊢ ( 𝐾 ∈ ℤ → ( ∀ 𝑘 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) [ ( 𝐾 − 𝑘 ) / 𝑗 ] 𝜑 → ∀ 𝑗 ∈ ( 𝑀 ... 𝑁 ) 𝜑 ) )
33 32 3ad2ant3 ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ∀ 𝑘 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) [ ( 𝐾 − 𝑘 ) / 𝑗 ] 𝜑 → ∀ 𝑗 ∈ ( 𝑀 ... 𝑁 ) 𝜑 ) )
34 11 33 impbid ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ∀ 𝑗 ∈ ( 𝑀 ... 𝑁 ) 𝜑 ↔ ∀ 𝑘 ∈ ( ( 𝐾 − 𝑁 ) ... ( 𝐾 − 𝑀 ) ) [ ( 𝐾 − 𝑘 ) / 𝑗 ] 𝜑 ) )