Definition df-nqqs 7716

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 7648	. 2 class Q
2		cnpi 7640	. . . 4 class N
3	2, 2	cxp 4772	. . 3 class (N × N)
4		ceq 7647	. . 3 class ~Q
5	3, 4	cqs 6806	. 2 class ((N × N) / ~Q )
6	1, 5	wceq 1402	1 wff Q = ((N × N) / ~Q )

This definition is used by:  nqex  7731  0nnq  7732  1nq  7734  addpipqqs  7738  mulpipqqs  7741  ordpipqqs  7742  addclnq  7743  mulclnq  7744  dmaddpqlem  7745  nqpi  7746  addcomnqg  7749  addassnqg  7750  mulcomnqg  7751  mulassnqg  7752  distrnqg  7755  mulidnq  7757  recexnq  7758  nqtri3or  7764  ltsonq  7766  ltanqg  7768  ltmnqg  7769  ltexnqq  7776  prarloclemarch  7786  prarloclemarch2  7787  nnnq  7790  nqnq0  7809  nqpnq0nq  7821  prarloclemlt  7861  prarloclemlo  7862  prarloclemcalc  7870  nqprm  7910