This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fzrev

Description: Reversal of start and end of a finite set of sequential integers. (Contributed by NM, 25-Nov-2005)

Ref Expression
Assertion fzrev ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → ( 𝐾 ∈ ( ( 𝐽 − 𝑁 ) ... ( 𝐽 − 𝑀 ) ) ↔ ( 𝐽 − 𝐾 ) ∈ ( 𝑀 ... 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 zre ⊢ ( 𝐽 ∈ ℤ → 𝐽 ∈ ℝ )
2 zre ⊢ ( 𝐾 ∈ ℤ → 𝐾 ∈ ℝ )
3 zre ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
4 suble ⊢ ( ( 𝐽 ∈ ℝ ∧ 𝐾 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( 𝐽 − 𝐾 ) ≤ 𝑁 ↔ ( 𝐽 − 𝑁 ) ≤ 𝐾 ) )
5 1 2 3 4 syl3an ⊢ ( ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐽 − 𝐾 ) ≤ 𝑁 ↔ ( 𝐽 − 𝑁 ) ≤ 𝐾 ) )
6 5 3comr ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( ( 𝐽 − 𝐾 ) ≤ 𝑁 ↔ ( 𝐽 − 𝑁 ) ≤ 𝐾 ) )
7 6 3expb ⊢ ( ( 𝑁 ∈ ℤ ∧ ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → ( ( 𝐽 − 𝐾 ) ≤ 𝑁 ↔ ( 𝐽 − 𝑁 ) ≤ 𝐾 ) )
8 7 adantll ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → ( ( 𝐽 − 𝐾 ) ≤ 𝑁 ↔ ( 𝐽 − 𝑁 ) ≤ 𝐾 ) )
9 zre ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ )
10 lesub ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝐽 ∈ ℝ ∧ 𝐾 ∈ ℝ ) → ( 𝑀 ≤ ( 𝐽 − 𝐾 ) ↔ 𝐾 ≤ ( 𝐽 − 𝑀 ) ) )
11 9 1 2 10 syl3an ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝑀 ≤ ( 𝐽 − 𝐾 ) ↔ 𝐾 ≤ ( 𝐽 − 𝑀 ) ) )
12 11 3expb ⊢ ( ( 𝑀 ∈ ℤ ∧ ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → ( 𝑀 ≤ ( 𝐽 − 𝐾 ) ↔ 𝐾 ≤ ( 𝐽 − 𝑀 ) ) )
13 12 adantlr ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → ( 𝑀 ≤ ( 𝐽 − 𝐾 ) ↔ 𝐾 ≤ ( 𝐽 − 𝑀 ) ) )
14 8 13 anbi12d ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → ( ( ( 𝐽 − 𝐾 ) ≤ 𝑁 ∧ 𝑀 ≤ ( 𝐽 − 𝐾 ) ) ↔ ( ( 𝐽 − 𝑁 ) ≤ 𝐾 ∧ 𝐾 ≤ ( 𝐽 − 𝑀 ) ) ) )
15 ancom ⊢ ( ( ( 𝐽 − 𝐾 ) ≤ 𝑁 ∧ 𝑀 ≤ ( 𝐽 − 𝐾 ) ) ↔ ( 𝑀 ≤ ( 𝐽 − 𝐾 ) ∧ ( 𝐽 − 𝐾 ) ≤ 𝑁 ) )
16 14 15 bitr3di ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → ( ( ( 𝐽 − 𝑁 ) ≤ 𝐾 ∧ 𝐾 ≤ ( 𝐽 − 𝑀 ) ) ↔ ( 𝑀 ≤ ( 𝐽 − 𝐾 ) ∧ ( 𝐽 − 𝐾 ) ≤ 𝑁 ) ) )
17 simprr ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → 𝐾 ∈ ℤ )
18 zsubcl ⊢ ( ( 𝐽 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐽 − 𝑁 ) ∈ ℤ )
19 18 ancoms ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝐽 ∈ ℤ ) → ( 𝐽 − 𝑁 ) ∈ ℤ )
20 19 ad2ant2lr ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → ( 𝐽 − 𝑁 ) ∈ ℤ )
21 zsubcl ⊢ ( ( 𝐽 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 𝐽 − 𝑀 ) ∈ ℤ )
22 21 ancoms ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐽 ∈ ℤ ) → ( 𝐽 − 𝑀 ) ∈ ℤ )
23 22 ad2ant2r ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → ( 𝐽 − 𝑀 ) ∈ ℤ )
24 elfz ⊢ ( ( 𝐾 ∈ ℤ ∧ ( 𝐽 − 𝑁 ) ∈ ℤ ∧ ( 𝐽 − 𝑀 ) ∈ ℤ ) → ( 𝐾 ∈ ( ( 𝐽 − 𝑁 ) ... ( 𝐽 − 𝑀 ) ) ↔ ( ( 𝐽 − 𝑁 ) ≤ 𝐾 ∧ 𝐾 ≤ ( 𝐽 − 𝑀 ) ) ) )
25 17 20 23 24 syl3anc ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → ( 𝐾 ∈ ( ( 𝐽 − 𝑁 ) ... ( 𝐽 − 𝑀 ) ) ↔ ( ( 𝐽 − 𝑁 ) ≤ 𝐾 ∧ 𝐾 ≤ ( 𝐽 − 𝑀 ) ) ) )
26 zsubcl ⊢ ( ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) → ( 𝐽 − 𝐾 ) ∈ ℤ )
27 26 adantl ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → ( 𝐽 − 𝐾 ) ∈ ℤ )
28 simpll ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → 𝑀 ∈ ℤ )
29 simplr ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → 𝑁 ∈ ℤ )
30 elfz ⊢ ( ( ( 𝐽 − 𝐾 ) ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝐽 − 𝐾 ) ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝑀 ≤ ( 𝐽 − 𝐾 ) ∧ ( 𝐽 − 𝐾 ) ≤ 𝑁 ) ) )
31 27 28 29 30 syl3anc ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → ( ( 𝐽 − 𝐾 ) ∈ ( 𝑀 ... 𝑁 ) ↔ ( 𝑀 ≤ ( 𝐽 − 𝐾 ) ∧ ( 𝐽 − 𝐾 ) ≤ 𝑁 ) ) )
32 16 25 31 3bitr4d ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → ( 𝐾 ∈ ( ( 𝐽 − 𝑁 ) ... ( 𝐽 − 𝑀 ) ) ↔ ( 𝐽 − 𝐾 ) ∈ ( 𝑀 ... 𝑁 ) ) )