Theorem 1xr

Description: 1 is an extended real number. (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Assertion	1xr	$$⊢1\in {ℝ}^{*}$$

Proof

Step	Hyp	Ref	Expression
1		1re	$$⊢1\in ℝ$$
2	1	rexri	$$⊢1\in {ℝ}^{*}$$