Theorem uzssre2

Description: An upper set of integers is a subset of the Reals. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypothesis	uzssre2.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
Assertion	uzssre2	$$⊢Z\subseteq ℝ$$

Proof

Step	Hyp	Ref	Expression
1		uzssre2.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
2		uzssz	$$⊢{\mathbb{Z}}_{\ge M}\subseteq \mathbb{Z}$$
3		zssre	$$⊢\mathbb{Z}\subseteq ℝ$$
4	2 3	sstri	$$⊢{\mathbb{Z}}_{\ge M}\subseteq ℝ$$
5	1 4	eqsstri	$$⊢Z\subseteq ℝ$$