This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem elfzouz

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

		Ref	Expression
	Assertion	elfzouz	$⊢ K \in (M ..^N) \to K \in ℤ_{\geq M}$

Step	Hyp	Ref	Expression
1		elfzo2	$⊢ K \in (M ..^N) \leftrightarrow (K \in ℤ_{\geq M} \land N \in ℤ \land K < N)$
2	1	simp1bi	$⊢ K \in (M ..^N) \to K \in ℤ_{\geq M}$