Theorem 1xr

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

	Ref	Expression
Assertion	1xr	⊢ 1 ∈ ℝ*

Proof

Step	Hyp	Ref	Expression
1		1re	⊢ 1 ∈ ℝ
2	1	rexri	⊢ 1 ∈ ℝ*