elfzo3

Description: Express membership in a half-open integer interval in terms of the "less than or equal to" and "less than" predicates on integers, resp. K e. ( ZZ>=M ) <-> M <_ K , K e. ( K ..^ N ) <-> K < N . (Contributed by Mario Carneiro, 29-Sep-2015)

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

Proof

Step	Hyp	Ref	Expression
1		3anass	$⊢ (K \in ℤ_{\geq M} \land N \in ℤ \land K < N) \leftrightarrow (K \in ℤ_{\geq M} \land (N \in ℤ \land K < N))$
2		elfzo2	$⊢ K \in (M ..^N) \leftrightarrow (K \in ℤ_{\geq M} \land N \in ℤ \land K < N)$
3		eluzelz	$⊢ K \in ℤ_{\geq M} \to K \in ℤ$
4		fzolb	$⊢ K \in (K ..^N) \leftrightarrow (K \in ℤ \land N \in ℤ \land K < N)$
5		3anass	$⊢ (K \in ℤ \land N \in ℤ \land K < N) \leftrightarrow (K \in ℤ \land (N \in ℤ \land K < N))$
6	4 5	bitri	$⊢ K \in (K ..^N) \leftrightarrow (K \in ℤ \land (N \in ℤ \land K < N))$
7	6	baib	$⊢ K \in ℤ \to (K \in (K ..^N) \leftrightarrow (N \in ℤ \land K < N))$
8	3 7	syl	$⊢ K \in ℤ_{\geq M} \to (K \in (K ..^N) \leftrightarrow (N \in ℤ \land K < N))$
9	8	pm5.32i	$⊢ (K \in ℤ_{\geq M} \land K \in (K ..^N)) \leftrightarrow (K \in ℤ_{\geq M} \land (N \in ℤ \land K < N))$
10	1 2 9	3bitr4i	$⊢ K \in (M ..^N) \leftrightarrow (K \in ℤ_{\geq M} \land K \in (K ..^N))$

Metamath Proof Explorer

Theorem elfzo3

Proof