Definition df-nqqs 7628

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 7560	. 2 class Q
2		cnpi 7552	. . . 4 class N
3	2, 2	cxp 4729	. . 3 class (N × N)
4		ceq 7559	. . 3 class ~Q
5	3, 4	cqs 6744	. 2 class ((N × N) / ~Q )
6	1, 5	wceq 1398	1 wff Q = ((N × N) / ~Q )

This definition is referenced by:  nqex  7643  0nnq  7644  1nq  7646  addpipqqs  7650  mulpipqqs  7653  ordpipqqs  7654  addclnq  7655  mulclnq  7656  dmaddpqlem  7657  nqpi  7658  addcomnqg  7661  addassnqg  7662  mulcomnqg  7663  mulassnqg  7664  distrnqg  7667  mulidnq  7669  recexnq  7670  nqtri3or  7676  ltsonq  7678  ltanqg  7680  ltmnqg  7681  ltexnqq  7688  prarloclemarch  7698  prarloclemarch2  7699  nnnq  7702  nqnq0  7721  nqpnq0nq  7733  prarloclemlt  7773  prarloclemlo  7774  prarloclemcalc  7782  nqprm  7822