Metamath Proof Explorer

Theorem elfzo2

Description: Membership in a half-open integer interval. (Contributed by Mario Carneiro, 29-Sep-2015)

		Ref	Expression
	Assertion	elfzo2	$⊢ K \in (M ..^N) \leftrightarrow (K \in ℤ_{\geq M} \land N \in ℤ \land K < N)$

Proof

Step	Hyp	Ref	Expression
1		an4	$⊢ (((K \in ℤ \land M \in ℤ) \land N \in ℤ) \land (M \leq K \land K < N)) \leftrightarrow (((K \in ℤ \land M \in ℤ) \land M \leq K) \land (N \in ℤ \land K < N))$
2		df-3an	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \leftrightarrow ((K \in ℤ \land M \in ℤ) \land N \in ℤ)$
3	2	anbi1i	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land (M \leq K \land K < N)) \leftrightarrow (((K \in ℤ \land M \in ℤ) \land N \in ℤ) \land (M \leq K \land K < N))$
4		eluz2	$⊢ K \in ℤ_{\geq M} \leftrightarrow (M \in ℤ \land K \in ℤ \land M \leq K)$
5		3ancoma	$⊢ (M \in ℤ \land K \in ℤ \land M \leq K) \leftrightarrow (K \in ℤ \land M \in ℤ \land M \leq K)$
6		df-3an	$⊢ (K \in ℤ \land M \in ℤ \land M \leq K) \leftrightarrow ((K \in ℤ \land M \in ℤ) \land M \leq K)$
7	4 5 6	3bitri	$⊢ K \in ℤ_{\geq M} \leftrightarrow ((K \in ℤ \land M \in ℤ) \land M \leq K)$
8	7	anbi1i	$⊢ (K \in ℤ_{\geq M} \land (N \in ℤ \land K < N)) \leftrightarrow (((K \in ℤ \land M \in ℤ) \land M \leq K) \land (N \in ℤ \land K < N))$
9	1 3 8	3bitr4i	$⊢ ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land (M \leq K \land K < N)) \leftrightarrow (K \in ℤ_{\geq M} \land (N \in ℤ \land K < N))$
10		elfzoelz	$⊢ K \in (M ..^N) \to K \in ℤ$
11		elfzoel1	$⊢ K \in (M ..^N) \to M \in ℤ$
12		elfzoel2	$⊢ K \in (M ..^N) \to N \in ℤ$
13	10 11 12	3jca	$⊢ K \in (M ..^N) \to (K \in ℤ \land M \in ℤ \land N \in ℤ)$
14		elfzo	$⊢ (K \in ℤ \land M \in ℤ \land N \in ℤ) \to (K \in (M ..^N) \leftrightarrow (M \leq K \land K < N))$
15	13 14	biadanii	$⊢ K \in (M ..^N) \leftrightarrow ((K \in ℤ \land M \in ℤ \land N \in ℤ) \land (M \leq K \land K < N))$
16		3anass	$⊢ (K \in ℤ_{\geq M} \land N \in ℤ \land K < N) \leftrightarrow (K \in ℤ_{\geq M} \land (N \in ℤ \land K < N))$
17	9 15 16	3bitr4i	$⊢ K \in (M ..^N) \leftrightarrow (K \in ℤ_{\geq M} \land N \in ℤ \land K < N)$