Theorem eluz1

Description: Membership in the upper set of integers starting at M . (Contributed by NM, 5-Sep-2005)

	Ref	Expression
Assertion	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)$$

Proof

Step	Hyp	Ref	Expression
1		uzval	$$⊢M\in \mathbb{Z}\to {\mathbb{Z}}_{\ge M}=\left\{k\in \mathbb{Z}|M\le k\right\}$$
2	1	eleq2d	$$⊢M\in \mathbb{Z}\to \left(N\in {\mathbb{Z}}_{\ge M}\leftrightarrow N\in \left\{k\in \mathbb{Z}|M\le k\right\}\right)$$
3		breq2	$$⊢k=N\to \left(M\le k\leftrightarrow M\le N\right)$$
4	3	elrab	$$⊢N\in \left\{k\in \mathbb{Z}|M\le k\right\}\leftrightarrow \left(N\in \mathbb{Z}\wedge M\le N\right)$$
5	2 4	bitrdi	$$⊢M\in \mathbb{Z}\to \left(N\in {\mathbb{Z}}_{\ge M}\leftrightarrow \left(N\in \mathbb{Z}\wedge M\le N\right)\right)$$