Theorem eluzd

Description: Membership in an upper set of integers. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	eluzd.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
	eluzd.2	$$⊢\phi \to M\in \mathbb{Z}$$
	eluzd.3	$$⊢\phi \to N\in \mathbb{Z}$$
	eluzd.4	$$⊢\phi \to M\le N$$
Assertion	eluzd	$$⊢\phi \to N\in Z$$

Proof

Step	Hyp	Ref	Expression
1		eluzd.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
2		eluzd.2	$$⊢\phi \to M\in \mathbb{Z}$$
3		eluzd.3	$$⊢\phi \to N\in \mathbb{Z}$$
4		eluzd.4	$$⊢\phi \to M\le N$$
5		eluz2	$$⊢N\in {\mathbb{Z}}_{\ge M}\leftrightarrow \left(M\in \mathbb{Z}\wedge N\in \mathbb{Z}\wedge M\le N\right)$$
6	2 3 4 5	syl3anbrc	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge M}$$
7	6 1	eleqtrrdi	$$⊢\phi \to N\in Z$$