Theorem eluzle

Description: Implication of membership in an upper set of integers. (Contributed by NM, 6-Sep-2005)

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

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	simp3bi	$$⊢N\in {\mathbb{Z}}_{\ge M}\to M\le N$$