Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Glauco Siliprandi
Ordering on real numbers - Real and complex numbers basic operations
nnxr
Next ⟩
abssubrp
Metamath Proof Explorer
Ascii
Structured
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
⊢
(
𝑁
∈ ℕ →
𝑁
∈ ℝ
*
)