Database
REAL AND COMPLEX NUMBERS
Integer sets
Rational numbers (as a subset of complex numbers)
nnssq
Next ⟩
qssre
Metamath Proof Explorer
Ascii
Unicode
Theorem
nnssq
Description:
The positive integers are a subset of the rationals.
(Contributed by
NM
, 31-Jul-2004)
Ref
Expression
Assertion
nnssq
⊢
ℕ
⊆
ℚ
Proof
Step
Hyp
Ref
Expression
1
nnssz
⊢
ℕ
⊆
ℤ
2
zssq
⊢
ℤ
⊆
ℚ
3
1
2
sstri
⊢
ℕ
⊆
ℚ