Metamath Proof Explorer


Theorem fzshftral

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

Ref Expression
Assertion fzshftral ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ∀ 𝑗 ∈ ( 𝑀 ... 𝑁 ) 𝜑 ↔ ∀ 𝑘 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) [ ( 𝑘𝐾 ) / 𝑗 ] 𝜑 ) )

Proof

Step Hyp Ref Expression
1 0z 0 ∈ ℤ
2 fzrevral ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 0 ∈ ℤ ) → ( ∀ 𝑗 ∈ ( 𝑀 ... 𝑁 ) 𝜑 ↔ ∀ 𝑥 ∈ ( ( 0 − 𝑁 ) ... ( 0 − 𝑀 ) ) [ ( 0 − 𝑥 ) / 𝑗 ] 𝜑 ) )
3 1 2 mp3an3 ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ∀ 𝑗 ∈ ( 𝑀 ... 𝑁 ) 𝜑 ↔ ∀ 𝑥 ∈ ( ( 0 − 𝑁 ) ... ( 0 − 𝑀 ) ) [ ( 0 − 𝑥 ) / 𝑗 ] 𝜑 ) )
4 3 3adant3 ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ∀ 𝑗 ∈ ( 𝑀 ... 𝑁 ) 𝜑 ↔ ∀ 𝑥 ∈ ( ( 0 − 𝑁 ) ... ( 0 − 𝑀 ) ) [ ( 0 − 𝑥 ) / 𝑗 ] 𝜑 ) )
5 zsubcl ( ( 0 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 0 − 𝑁 ) ∈ ℤ )
6 1 5 mpan ( 𝑁 ∈ ℤ → ( 0 − 𝑁 ) ∈ ℤ )
7 zsubcl ( ( 0 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 0 − 𝑀 ) ∈ ℤ )
8 1 7 mpan ( 𝑀 ∈ ℤ → ( 0 − 𝑀 ) ∈ ℤ )
9 id ( 𝐾 ∈ ℤ → 𝐾 ∈ ℤ )
10 fzrevral ( ( ( 0 − 𝑁 ) ∈ ℤ ∧ ( 0 − 𝑀 ) ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ∀ 𝑥 ∈ ( ( 0 − 𝑁 ) ... ( 0 − 𝑀 ) ) [ ( 0 − 𝑥 ) / 𝑗 ] 𝜑 ↔ ∀ 𝑘 ∈ ( ( 𝐾 − ( 0 − 𝑀 ) ) ... ( 𝐾 − ( 0 − 𝑁 ) ) ) [ ( 𝐾𝑘 ) / 𝑥 ] [ ( 0 − 𝑥 ) / 𝑗 ] 𝜑 ) )
11 6 8 9 10 syl3an ( ( 𝑁 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ∀ 𝑥 ∈ ( ( 0 − 𝑁 ) ... ( 0 − 𝑀 ) ) [ ( 0 − 𝑥 ) / 𝑗 ] 𝜑 ↔ ∀ 𝑘 ∈ ( ( 𝐾 − ( 0 − 𝑀 ) ) ... ( 𝐾 − ( 0 − 𝑁 ) ) ) [ ( 𝐾𝑘 ) / 𝑥 ] [ ( 0 − 𝑥 ) / 𝑗 ] 𝜑 ) )
12 11 3com12 ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ∀ 𝑥 ∈ ( ( 0 − 𝑁 ) ... ( 0 − 𝑀 ) ) [ ( 0 − 𝑥 ) / 𝑗 ] 𝜑 ↔ ∀ 𝑘 ∈ ( ( 𝐾 − ( 0 − 𝑀 ) ) ... ( 𝐾 − ( 0 − 𝑁 ) ) ) [ ( 𝐾𝑘 ) / 𝑥 ] [ ( 0 − 𝑥 ) / 𝑗 ] 𝜑 ) )
13 ovex ( 𝐾𝑘 ) ∈ V
14 oveq2 ( 𝑥 = ( 𝐾𝑘 ) → ( 0 − 𝑥 ) = ( 0 − ( 𝐾𝑘 ) ) )
15 14 sbcco3gw ( ( 𝐾𝑘 ) ∈ V → ( [ ( 𝐾𝑘 ) / 𝑥 ] [ ( 0 − 𝑥 ) / 𝑗 ] 𝜑[ ( 0 − ( 𝐾𝑘 ) ) / 𝑗 ] 𝜑 ) )
16 13 15 ax-mp ( [ ( 𝐾𝑘 ) / 𝑥 ] [ ( 0 − 𝑥 ) / 𝑗 ] 𝜑[ ( 0 − ( 𝐾𝑘 ) ) / 𝑗 ] 𝜑 )
17 16 ralbii ( ∀ 𝑘 ∈ ( ( 𝐾 − ( 0 − 𝑀 ) ) ... ( 𝐾 − ( 0 − 𝑁 ) ) ) [ ( 𝐾𝑘 ) / 𝑥 ] [ ( 0 − 𝑥 ) / 𝑗 ] 𝜑 ↔ ∀ 𝑘 ∈ ( ( 𝐾 − ( 0 − 𝑀 ) ) ... ( 𝐾 − ( 0 − 𝑁 ) ) ) [ ( 0 − ( 𝐾𝑘 ) ) / 𝑗 ] 𝜑 )
18 zcn ( 𝑀 ∈ ℤ → 𝑀 ∈ ℂ )
19 zcn ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
20 zcn ( 𝐾 ∈ ℤ → 𝐾 ∈ ℂ )
21 df-neg - 𝑀 = ( 0 − 𝑀 )
22 21 oveq2i ( 𝐾 − - 𝑀 ) = ( 𝐾 − ( 0 − 𝑀 ) )
23 subneg ( ( 𝐾 ∈ ℂ ∧ 𝑀 ∈ ℂ ) → ( 𝐾 − - 𝑀 ) = ( 𝐾 + 𝑀 ) )
24 addcom ( ( 𝐾 ∈ ℂ ∧ 𝑀 ∈ ℂ ) → ( 𝐾 + 𝑀 ) = ( 𝑀 + 𝐾 ) )
25 23 24 eqtrd ( ( 𝐾 ∈ ℂ ∧ 𝑀 ∈ ℂ ) → ( 𝐾 − - 𝑀 ) = ( 𝑀 + 𝐾 ) )
26 22 25 eqtr3id ( ( 𝐾 ∈ ℂ ∧ 𝑀 ∈ ℂ ) → ( 𝐾 − ( 0 − 𝑀 ) ) = ( 𝑀 + 𝐾 ) )
27 26 3adant3 ( ( 𝐾 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( 𝐾 − ( 0 − 𝑀 ) ) = ( 𝑀 + 𝐾 ) )
28 df-neg - 𝑁 = ( 0 − 𝑁 )
29 28 oveq2i ( 𝐾 − - 𝑁 ) = ( 𝐾 − ( 0 − 𝑁 ) )
30 subneg ( ( 𝐾 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( 𝐾 − - 𝑁 ) = ( 𝐾 + 𝑁 ) )
31 addcom ( ( 𝐾 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( 𝐾 + 𝑁 ) = ( 𝑁 + 𝐾 ) )
32 30 31 eqtrd ( ( 𝐾 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( 𝐾 − - 𝑁 ) = ( 𝑁 + 𝐾 ) )
33 29 32 eqtr3id ( ( 𝐾 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( 𝐾 − ( 0 − 𝑁 ) ) = ( 𝑁 + 𝐾 ) )
34 33 3adant2 ( ( 𝐾 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( 𝐾 − ( 0 − 𝑁 ) ) = ( 𝑁 + 𝐾 ) )
35 27 34 oveq12d ( ( 𝐾 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( ( 𝐾 − ( 0 − 𝑀 ) ) ... ( 𝐾 − ( 0 − 𝑁 ) ) ) = ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) )
36 35 3coml ( ( 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ 𝐾 ∈ ℂ ) → ( ( 𝐾 − ( 0 − 𝑀 ) ) ... ( 𝐾 − ( 0 − 𝑁 ) ) ) = ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) )
37 18 19 20 36 syl3an ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ( 𝐾 − ( 0 − 𝑀 ) ) ... ( 𝐾 − ( 0 − 𝑁 ) ) ) = ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) )
38 37 raleqdv ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ∀ 𝑘 ∈ ( ( 𝐾 − ( 0 − 𝑀 ) ) ... ( 𝐾 − ( 0 − 𝑁 ) ) ) [ ( 0 − ( 𝐾𝑘 ) ) / 𝑗 ] 𝜑 ↔ ∀ 𝑘 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) [ ( 0 − ( 𝐾𝑘 ) ) / 𝑗 ] 𝜑 ) )
39 elfzelz ( 𝑘 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) → 𝑘 ∈ ℤ )
40 39 zcnd ( 𝑘 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) → 𝑘 ∈ ℂ )
41 df-neg - ( 𝐾𝑘 ) = ( 0 − ( 𝐾𝑘 ) )
42 negsubdi2 ( ( 𝐾 ∈ ℂ ∧ 𝑘 ∈ ℂ ) → - ( 𝐾𝑘 ) = ( 𝑘𝐾 ) )
43 41 42 eqtr3id ( ( 𝐾 ∈ ℂ ∧ 𝑘 ∈ ℂ ) → ( 0 − ( 𝐾𝑘 ) ) = ( 𝑘𝐾 ) )
44 20 40 43 syl2an ( ( 𝐾 ∈ ℤ ∧ 𝑘 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ) → ( 0 − ( 𝐾𝑘 ) ) = ( 𝑘𝐾 ) )
45 44 sbceq1d ( ( 𝐾 ∈ ℤ ∧ 𝑘 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) ) → ( [ ( 0 − ( 𝐾𝑘 ) ) / 𝑗 ] 𝜑[ ( 𝑘𝐾 ) / 𝑗 ] 𝜑 ) )
46 45 ralbidva ( 𝐾 ∈ ℤ → ( ∀ 𝑘 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) [ ( 0 − ( 𝐾𝑘 ) ) / 𝑗 ] 𝜑 ↔ ∀ 𝑘 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) [ ( 𝑘𝐾 ) / 𝑗 ] 𝜑 ) )
47 46 3ad2ant3 ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ∀ 𝑘 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) [ ( 0 − ( 𝐾𝑘 ) ) / 𝑗 ] 𝜑 ↔ ∀ 𝑘 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) [ ( 𝑘𝐾 ) / 𝑗 ] 𝜑 ) )
48 38 47 bitrd ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ∀ 𝑘 ∈ ( ( 𝐾 − ( 0 − 𝑀 ) ) ... ( 𝐾 − ( 0 − 𝑁 ) ) ) [ ( 0 − ( 𝐾𝑘 ) ) / 𝑗 ] 𝜑 ↔ ∀ 𝑘 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) [ ( 𝑘𝐾 ) / 𝑗 ] 𝜑 ) )
49 17 48 syl5bb ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ∀ 𝑘 ∈ ( ( 𝐾 − ( 0 − 𝑀 ) ) ... ( 𝐾 − ( 0 − 𝑁 ) ) ) [ ( 𝐾𝑘 ) / 𝑥 ] [ ( 0 − 𝑥 ) / 𝑗 ] 𝜑 ↔ ∀ 𝑘 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) [ ( 𝑘𝐾 ) / 𝑗 ] 𝜑 ) )
50 4 12 49 3bitrd ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ∀ 𝑗 ∈ ( 𝑀 ... 𝑁 ) 𝜑 ↔ ∀ 𝑘 ∈ ( ( 𝑀 + 𝐾 ) ... ( 𝑁 + 𝐾 ) ) [ ( 𝑘𝐾 ) / 𝑗 ] 𝜑 ) )