Theorem uzxrd

Description: An upper integer is an extended real. (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Hypotheses	uzxrd.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
	uzxrd.2	$$⊢\phi \to A\in Z$$
Assertion	uzxrd	$$⊢\phi \to A\in {ℝ}^{*}$$

Proof

Step	Hyp	Ref	Expression
1		uzxrd.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
2		uzxrd.2	$$⊢\phi \to A\in Z$$
3		ressxr	$$⊢ℝ\subseteq {ℝ}^{*}$$
4	1 2	uzred	$$⊢\phi \to A\in ℝ$$
5	3 4	sselid	$$⊢\phi \to A\in {ℝ}^{*}$$