Metamath Proof Explorer


Theorem 1q

Description: The number 1 is rational. (Contributed by SN, 30-Aug-2026)

Ref Expression
Assertion 1q
|- 1 e. QQ

Proof

Step Hyp Ref Expression
1 zssq
 |-  ZZ C_ QQ
2 1z
 |-  1 e. ZZ
3 1 2 sselii
 |-  1 e. QQ