Theorem elfzouz

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

	Ref	Expression
Assertion	elfzouz	$$⊢K\in \left(M..^N\right)\to K\in {\mathbb{Z}}_{\ge M}$$

Proof

Step	Hyp	Ref	Expression
1		elfzo2	$$⊢K\in \left(M..^N\right)\leftrightarrow \left(K\in {\mathbb{Z}}_{\ge M}\wedge N\in \mathbb{Z}\wedge K<N\right)$$
2	1	simp1bi	$$⊢K\in \left(M..^N\right)\to K\in {\mathbb{Z}}_{\ge M}$$