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

Proof

Step Hyp Ref Expression
1 id N N
2 1 nnxrd N N *