fzrev2i

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

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

Step	Hyp	Ref	Expression
1		simpr	$⊢ (J \in ℤ \land K \in (M \dots N)) \to K \in (M \dots N)$
2		elfzel1	$⊢ K \in (M \dots N) \to M \in ℤ$
3	2	adantl	$⊢ (J \in ℤ \land K \in (M \dots N)) \to M \in ℤ$
4		elfzel2	$⊢ K \in (M \dots N) \to N \in ℤ$
5	4	adantl	$⊢ (J \in ℤ \land K \in (M \dots N)) \to N \in ℤ$
6		simpl	$⊢ (J \in ℤ \land K \in (M \dots N)) \to J \in ℤ$
7		elfzelz	$⊢ K \in (M \dots N) \to K \in ℤ$
8	7	adantl	$⊢ (J \in ℤ \land K \in (M \dots N)) \to K \in ℤ$
9		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))$
10	3 5 6 8 9	syl22anc	$⊢ (J \in ℤ \land K \in (M \dots N)) \to (K \in (M \dots N) \leftrightarrow J - K \in (J - N \dots J - M))$
11	1 10	mpbid	$⊢ (J \in ℤ \land K \in (M \dots N)) \to J - K \in (J - N \dots J - M)$

Metamath Proof Explorer