Metamath Proof Explorer

Theorem elfzuzb

Description: Membership in a finite set of sequential integers in terms of sets of upper integers. (Contributed by NM, 18-Sep-2005) (Revised by Mario Carneiro, 28-Apr-2015)

		Ref	Expression
	Assertion	elfzuzb	$⊢ K \in (M \dots N) \leftrightarrow (K \in ℤ_{\geq M} \land N \in ℤ_{\geq K})$

Proof

Step	Hyp	Ref	Expression
1		df-3an	$⊢ ((M \in ℤ \land K \in ℤ) \land (K \in ℤ \land N \in ℤ) \land (M \leq K \land K \leq N)) \leftrightarrow (((M \in ℤ \land K \in ℤ) \land (K \in ℤ \land N \in ℤ)) \land (M \leq K \land K \leq N))$
2		an6	$⊢ ((M \in ℤ \land K \in ℤ \land M \leq K) \land (K \in ℤ \land N \in ℤ \land K \leq N)) \leftrightarrow ((M \in ℤ \land K \in ℤ) \land (K \in ℤ \land N \in ℤ) \land (M \leq K \land K \leq N))$
3		df-3an	$⊢ (M \in ℤ \land N \in ℤ \land K \in ℤ) \leftrightarrow ((M \in ℤ \land N \in ℤ) \land K \in ℤ)$
4		anandir	$⊢ ((M \in ℤ \land N \in ℤ) \land K \in ℤ) \leftrightarrow ((M \in ℤ \land K \in ℤ) \land (N \in ℤ \land K \in ℤ))$
5		an43	$⊢ ((M \in ℤ \land K \in ℤ) \land (N \in ℤ \land K \in ℤ)) \leftrightarrow ((M \in ℤ \land K \in ℤ) \land (K \in ℤ \land N \in ℤ))$
6	3 4 5	3bitri	$⊢ (M \in ℤ \land N \in ℤ \land K \in ℤ) \leftrightarrow ((M \in ℤ \land K \in ℤ) \land (K \in ℤ \land N \in ℤ))$
7	6	anbi1i	$⊢ ((M \in ℤ \land N \in ℤ \land K \in ℤ) \land (M \leq K \land K \leq N)) \leftrightarrow (((M \in ℤ \land K \in ℤ) \land (K \in ℤ \land N \in ℤ)) \land (M \leq K \land K \leq N))$
8	1 2 7	3bitr4ri	$⊢ ((M \in ℤ \land N \in ℤ \land K \in ℤ) \land (M \leq K \land K \leq N)) \leftrightarrow ((M \in ℤ \land K \in ℤ \land M \leq K) \land (K \in ℤ \land N \in ℤ \land K \leq N))$
9		elfz2	$⊢ K \in (M \dots N) \leftrightarrow ((M \in ℤ \land N \in ℤ \land K \in ℤ) \land (M \leq K \land K \leq N))$
10		eluz2	$⊢ K \in ℤ_{\geq M} \leftrightarrow (M \in ℤ \land K \in ℤ \land M \leq K)$
11		eluz2	$⊢ N \in ℤ_{\geq K} \leftrightarrow (K \in ℤ \land N \in ℤ \land K \leq N)$
12	10 11	anbi12i	$⊢ (K \in ℤ_{\geq M} \land N \in ℤ_{\geq K}) \leftrightarrow ((M \in ℤ \land K \in ℤ \land M \leq K) \land (K \in ℤ \land N \in ℤ \land K \leq N))$
13	8 9 12	3bitr4i	$⊢ K \in (M \dots N) \leftrightarrow (K \in ℤ_{\geq M} \land N \in ℤ_{\geq K})$