Metamath Proof Explorer


Theorem nnxr

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

Ref Expression
Assertion nnxr ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ* )

Proof

Step Hyp Ref Expression
1 id ( 𝑁 ∈ ℕ → 𝑁 ∈ ℕ )
2 1 nnxrd ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ* )