Theorem 1xr

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

	Ref	Expression
Assertion	1xr	|- 1 e. RR*

Proof

Step	Hyp	Ref	Expression
1		1re	|- 1 e. RR
2	1	rexri	|- 1 e. RR*