This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ℝ* )