Definition df-nqqs 7347

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 7279	. 2 class Q
2		cnpi 7271	. . . 4 class N
3	2, 2	cxp 4625	. . 3 class (N × N)
4		ceq 7278	. . 3 class ~Q
5	3, 4	cqs 6534	. 2 class ((N × N) / ~Q )
6	1, 5	wceq 1353	1 wff Q = ((N × N) / ~Q )

This definition is referenced by:  nqex  7362  0nnq  7363  1nq  7365  addpipqqs  7369  mulpipqqs  7372  ordpipqqs  7373  addclnq  7374  mulclnq  7375  dmaddpqlem  7376  nqpi  7377  addcomnqg  7380  addassnqg  7381  mulcomnqg  7382  mulassnqg  7383  distrnqg  7386  mulidnq  7388  recexnq  7389  nqtri3or  7395  ltsonq  7397  ltanqg  7399  ltmnqg  7400  ltexnqq  7407  prarloclemarch  7417  prarloclemarch2  7418  nnnq  7421  nqnq0  7440  nqpnq0nq  7452  prarloclemlt  7492  prarloclemlo  7493  prarloclemcalc  7501  nqprm  7541