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 ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( 𝐽 ∈ ℤ ∧ 𝐾 ∈ ℤ ) ) → ( 𝐾 ∈ ( ( 𝐽𝑁 ) ... ( 𝐽𝑀 ) ) ↔ ( 𝐽𝐾 ) ∈ ( 𝑀 ... 𝑁 ) ) )