Metamath Proof Explorer


Definition df-q

Description: Define the set of rational numbers. Based on definition of rationals in Apostol p. 22. See elq for the relation "is rational". (Contributed by NM, 8-Jan-2002)

Ref Expression
Assertion df-q
|- QQ = ( / " ( ZZ X. NN ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cq
 |-  QQ
1 cdiv
 |-  /
2 cz
 |-  ZZ
3 cn
 |-  NN
4 2 3 cxp
 |-  ( ZZ X. NN )
5 1 4 cima
 |-  ( / " ( ZZ X. NN ) )
6 0 5 wceq
 |-  QQ = ( / " ( ZZ X. NN ) )