elfz1

Description: Membership in a finite set of sequential integers. (Contributed by NM, 21-Jul-2005)

		Ref	Expression
	Assertion	elfz1	$⊢ (M \in ℤ \land N \in ℤ) \to (K \in (M \dots N) \leftrightarrow (K \in ℤ \land M \leq K \land K \leq N))$

Step	Hyp	Ref	Expression
1		fzval	$⊢ (M \in ℤ \land N \in ℤ) \to (M \dots N) = \{j \in ℤ \| (M \leq j \land j \leq N)\}$
2	1	eleq2d	$⊢ (M \in ℤ \land N \in ℤ) \to (K \in (M \dots N) \leftrightarrow K \in \{j \in ℤ \| (M \leq j \land j \leq N)\})$
3		breq2	$⊢ j = K \to (M \leq j \leftrightarrow M \leq K)$
4		breq1	$⊢ j = K \to (j \leq N \leftrightarrow K \leq N)$
5	3 4	anbi12d	$⊢ j = K \to ((M \leq j \land j \leq N) \leftrightarrow (M \leq K \land K \leq N))$
6	5	elrab	$⊢ K \in \{j \in ℤ \| (M \leq j \land j \leq N)\} \leftrightarrow (K \in ℤ \land (M \leq K \land K \leq N))$
7		3anass	$⊢ (K \in ℤ \land M \leq K \land K \leq N) \leftrightarrow (K \in ℤ \land (M \leq K \land K \leq N))$
8	6 7	bitr4i	$⊢ K \in \{j \in ℤ \| (M \leq j \land j \leq N)\} \leftrightarrow (K \in ℤ \land M \leq K \land K \leq N)$
9	2 8	bitrdi	$⊢ (M \in ℤ \land N \in ℤ) \to (K \in (M \dots N) \leftrightarrow (K \in ℤ \land M \leq K \land K \leq N))$

Metamath Proof Explorer