Metamath Proof Explorer


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