Database
REAL AND COMPLEX NUMBERS
Integer sets
Rational numbers (as a subset of complex numbers)
1q
Next ⟩
qaddcl
Metamath Proof Explorer
Ascii
Unicode
Theorem
1q
Description:
The number 1 is rational.
(Contributed by
SN
, 30-Aug-2026)
Ref
Expression
Assertion
1q
⊢
1
∈
ℚ
Proof
Step
Hyp
Ref
Expression
1
zssq
⊢
ℤ
⊆
ℚ
2
1z
⊢
1
∈
ℤ
3
1
2
sselii
⊢
1
∈
ℚ