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