Theorem eluzelz

Description: A member of an upper set of integers is an integer. (Contributed by NM, 6-Sep-2005)

	Ref	Expression
Assertion	eluzelz	$$⊢N\in {\mathbb{Z}}_{\ge M}\to N\in \mathbb{Z}$$

Proof

Step	Hyp	Ref	Expression
1		eluz2	$$⊢N\in {\mathbb{Z}}_{\ge M}\leftrightarrow \left(M\in \mathbb{Z}\wedge N\in \mathbb{Z}\wedge M\le N\right)$$
2	1	simp2bi	$$⊢N\in {\mathbb{Z}}_{\ge M}\to N\in \mathbb{Z}$$