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 ∈ ℚ