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* )