fzrev

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

		Ref	Expression
	Assertion	fzrev	$⊢ ((M \in ℤ \land N \in ℤ) \land (J \in ℤ \land K \in ℤ)) \to (K \in (J - N \dots J - M) \leftrightarrow J - K \in (M \dots N))$

Proof

Step	Hyp	Ref	Expression
1		zre	$⊢ J \in ℤ \to J \in ℝ$
2		zre	$⊢ K \in ℤ \to K \in ℝ$
3		zre	$⊢ N \in ℤ \to N \in ℝ$
4		suble	$⊢ (J \in ℝ \land K \in ℝ \land N \in ℝ) \to (J - K \leq N \leftrightarrow J - N \leq K)$
5	1 2 3 4	syl3an	$⊢ (J \in ℤ \land K \in ℤ \land N \in ℤ) \to (J - K \leq N \leftrightarrow J - N \leq K)$
6	5	3comr	$⊢ (N \in ℤ \land J \in ℤ \land K \in ℤ) \to (J - K \leq N \leftrightarrow J - N \leq K)$
7	6	3expb	$⊢ (N \in ℤ \land (J \in ℤ \land K \in ℤ)) \to (J - K \leq N \leftrightarrow J - N \leq K)$
8	7	adantll	$⊢ ((M \in ℤ \land N \in ℤ) \land (J \in ℤ \land K \in ℤ)) \to (J - K \leq N \leftrightarrow J - N \leq K)$
9		zre	$⊢ M \in ℤ \to M \in ℝ$
10		lesub	$⊢ (M \in ℝ \land J \in ℝ \land K \in ℝ) \to (M \leq J - K \leftrightarrow K \leq J - M)$
11	9 1 2 10	syl3an	$⊢ (M \in ℤ \land J \in ℤ \land K \in ℤ) \to (M \leq J - K \leftrightarrow K \leq J - M)$
12	11	3expb	$⊢ (M \in ℤ \land (J \in ℤ \land K \in ℤ)) \to (M \leq J - K \leftrightarrow K \leq J - M)$
13	12	adantlr	$⊢ ((M \in ℤ \land N \in ℤ) \land (J \in ℤ \land K \in ℤ)) \to (M \leq J - K \leftrightarrow K \leq J - M)$
14	8 13	anbi12d	$⊢ ((M \in ℤ \land N \in ℤ) \land (J \in ℤ \land K \in ℤ)) \to ((J - K \leq N \land M \leq J - K) \leftrightarrow (J - N \leq K \land K \leq J - M))$
15		ancom	$⊢ (J - K \leq N \land M \leq J - K) \leftrightarrow (M \leq J - K \land J - K \leq N)$
16	14 15	bitr3di	$⊢ ((M \in ℤ \land N \in ℤ) \land (J \in ℤ \land K \in ℤ)) \to ((J - N \leq K \land K \leq J - M) \leftrightarrow (M \leq J - K \land J - K \leq N))$
17		simprr	$⊢ ((M \in ℤ \land N \in ℤ) \land (J \in ℤ \land K \in ℤ)) \to K \in ℤ$
18		zsubcl	$⊢ (J \in ℤ \land N \in ℤ) \to J - N \in ℤ$
19	18	ancoms	$⊢ (N \in ℤ \land J \in ℤ) \to J - N \in ℤ$
20	19	ad2ant2lr	$⊢ ((M \in ℤ \land N \in ℤ) \land (J \in ℤ \land K \in ℤ)) \to J - N \in ℤ$
21		zsubcl	$⊢ (J \in ℤ \land M \in ℤ) \to J - M \in ℤ$
22	21	ancoms	$⊢ (M \in ℤ \land J \in ℤ) \to J - M \in ℤ$
23	22	ad2ant2r	$⊢ ((M \in ℤ \land N \in ℤ) \land (J \in ℤ \land K \in ℤ)) \to J - M \in ℤ$
24		elfz	$⊢ (K \in ℤ \land J - N \in ℤ \land J - M \in ℤ) \to (K \in (J - N \dots J - M) \leftrightarrow (J - N \leq K \land K \leq J - M))$
25	17 20 23 24	syl3anc	$⊢ ((M \in ℤ \land N \in ℤ) \land (J \in ℤ \land K \in ℤ)) \to (K \in (J - N \dots J - M) \leftrightarrow (J - N \leq K \land K \leq J - M))$
26		zsubcl	$⊢ (J \in ℤ \land K \in ℤ) \to J - K \in ℤ$
27	26	adantl	$⊢ ((M \in ℤ \land N \in ℤ) \land (J \in ℤ \land K \in ℤ)) \to J - K \in ℤ$
28		simpll	$⊢ ((M \in ℤ \land N \in ℤ) \land (J \in ℤ \land K \in ℤ)) \to M \in ℤ$
29		simplr	$⊢ ((M \in ℤ \land N \in ℤ) \land (J \in ℤ \land K \in ℤ)) \to N \in ℤ$
30		elfz	$⊢ (J - K \in ℤ \land M \in ℤ \land N \in ℤ) \to (J - K \in (M \dots N) \leftrightarrow (M \leq J - K \land J - K \leq N))$
31	27 28 29 30	syl3anc	$⊢ ((M \in ℤ \land N \in ℤ) \land (J \in ℤ \land K \in ℤ)) \to (J - K \in (M \dots N) \leftrightarrow (M \leq J - K \land J - K \leq N))$
32	16 25 31	3bitr4d	$⊢ ((M \in ℤ \land N \in ℤ) \land (J \in ℤ \land K \in ℤ)) \to (K \in (J - N \dots J - M) \leftrightarrow J - K \in (M \dots N))$

Metamath Proof Explorer

Theorem fzrev

Proof