Metamath Proof Explorer

Theorem nnxr

Description: A natural number is an extended real. (Contributed by Glauco Siliprandi, 24-Jan-2025)

Ref Expression
Assertion nnxr 
|- ( N e. NN -> N e. RR* )

Proof

Step Hyp Ref Expression
1 id 
 |-  ( N e. NN -> N e. NN )
2 1 nnxrd 
 |-  ( N e. NN -> N e. RR* )