Theorem eluz

Description: Membership in an upper set of integers. (Contributed by NM, 2-Oct-2005)

	Ref	Expression
Assertion	eluz	$$⊢\left(M\in \mathbb{Z}\wedge N\in \mathbb{Z}\right)\to \left(N\in {\mathbb{Z}}_{\ge M}\leftrightarrow M\le N\right)$$

Proof

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