Definition df-nqqs 7460

Description: Define class of positive fractions. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. From Proposition 9-2.2 of [Gleason] p. 117. (Contributed by NM, 16-Aug-1995.)

Assertion

Ref	Expression
df-nqqs	⊢ Q = ((N × N) / ~Q )

Detailed syntax breakdown of Definition df-nqqs

Step	Hyp	Ref	Expression
1		cnq 7392	. 2 class Q
2		cnpi 7384	. . . 4 class N
3	2, 2	cxp 4672	. . 3 class (N × N)
4		ceq 7391	. . 3 class ~Q
5	3, 4	cqs 6618	. 2 class ((N × N) / ~Q )
6	1, 5	wceq 1372	1 wff Q = ((N × N) / ~Q )

This definition is referenced by:  nqex  7475  0nnq  7476  1nq  7478  addpipqqs  7482  mulpipqqs  7485  ordpipqqs  7486  addclnq  7487  mulclnq  7488  dmaddpqlem  7489  nqpi  7490  addcomnqg  7493  addassnqg  7494  mulcomnqg  7495  mulassnqg  7496  distrnqg  7499  mulidnq  7501  recexnq  7502  nqtri3or  7508  ltsonq  7510  ltanqg  7512  ltmnqg  7513  ltexnqq  7520  prarloclemarch  7530  prarloclemarch2  7531  nnnq  7534  nqnq0  7553  nqpnq0nq  7565  prarloclemlt  7605  prarloclemlo  7606  prarloclemcalc  7614  nqprm  7654