Database
REAL AND COMPLEX NUMBERS
Integer sets
Rational numbers (as a subset of complex numbers)
nnq
Next ⟩
qcn
Metamath Proof Explorer
Ascii
Unicode
Theorem
nnq
Description:
A positive integer is rational.
(Contributed by
NM
, 17-Nov-2004)
Ref
Expression
Assertion
nnq
⊢
A
∈
ℕ
→
A
∈
ℚ
Proof
Step
Hyp
Ref
Expression
1
nnssq
⊢
ℕ
⊆
ℚ
2
1
sseli
⊢
A
∈
ℕ
→
A
∈
ℚ