fzrev2

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

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

Step	Hyp	Ref	Expression
1		simpl	$⊢ (J \in ℤ \land K \in ℤ) \to J \in ℤ$
2		zsubcl	$⊢ (J \in ℤ \land K \in ℤ) \to J - K \in ℤ$
3	1 2	jca	$⊢ (J \in ℤ \land K \in ℤ) \to (J \in ℤ \land J - K \in ℤ)$
4		fzrev	$⊢ ((M \in ℤ \land N \in ℤ) \land (J \in ℤ \land J - K \in ℤ)) \to (J - K \in (J - N \dots J - M) \leftrightarrow J - (J - K) \in (M \dots N))$
5	3 4	sylan2	$⊢ ((M \in ℤ \land N \in ℤ) \land (J \in ℤ \land K \in ℤ)) \to (J - K \in (J - N \dots J - M) \leftrightarrow J - (J - K) \in (M \dots N))$
6		zcn	$⊢ J \in ℤ \to J \in ℂ$
7		zcn	$⊢ K \in ℤ \to K \in ℂ$
8		nncan	$⊢ (J \in ℂ \land K \in ℂ) \to J - (J - K) = K$
9	6 7 8	syl2an	$⊢ (J \in ℤ \land K \in ℤ) \to J - (J - K) = K$
10	9	adantl	$⊢ ((M \in ℤ \land N \in ℤ) \land (J \in ℤ \land K \in ℤ)) \to J - (J - K) = K$
11	10	eleq1d	$⊢ ((M \in ℤ \land N \in ℤ) \land (J \in ℤ \land K \in ℤ)) \to (J - (J - K) \in (M \dots N) \leftrightarrow K \in (M \dots N))$
12	5 11	bitr2d	$⊢ ((M \in ℤ \land N \in ℤ) \land (J \in ℤ \land K \in ℤ)) \to (K \in (M \dots N) \leftrightarrow J - K \in (J - N \dots J - M))$

Metamath Proof Explorer