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