Metamath Proof Explorer


Theorem nnxrd

Description: A natural number is an extended real. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypothesis nnxrd.1
|- ( ph -> A e. NN )
Assertion nnxrd
|- ( ph -> A e. RR* )

Proof

Step Hyp Ref Expression
1 nnxrd.1
 |-  ( ph -> A e. NN )
2 1 nnred
 |-  ( ph -> A e. RR )
3 2 rexrd
 |-  ( ph -> A e. RR* )