Database
REAL AND COMPLEX NUMBERS
Integer sets
Positive integers (as a subset of complex numbers)
nnred
Next ⟩
nncnd
Metamath Proof Explorer
Ascii
Unicode
Theorem
nnred
Description:
A positive integer is a real number.
(Contributed by
Mario Carneiro
, 27-May-2016)
Ref
Expression
Hypothesis
nnred.1
⊢
φ
→
A
∈
ℕ
Assertion
nnred
⊢
φ
→
A
∈
ℝ
Proof
Step
Hyp
Ref
Expression
1
nnred.1
⊢
φ
→
A
∈
ℕ
2
nnssre
⊢
ℕ
⊆
ℝ
3
2
1
sseldi
⊢
φ
→
A
∈
ℝ