Database
REAL AND COMPLEX NUMBERS
Integer sets
Positive integers (as a subset of complex numbers)
nnre
Next ⟩
nncn
Metamath Proof Explorer
Ascii
Structured
Theorem
nnre
Description:
A positive integer is a real number.
(Contributed by
NM
, 18-Aug-1999)
Ref
Expression
Assertion
nnre
⊢
(
𝐴
∈ ℕ →
𝐴
∈ ℝ )
Proof
Step
Hyp
Ref
Expression
1
nnssre
⊢
ℕ ⊆ ℝ
2
1
sseli
⊢
(
𝐴
∈ ℕ →
𝐴
∈ ℝ )