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