Definition df-nqqs 6332

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. X. N.) /. ~Q )

Detailed syntax breakdown of Definition df-nqqs

Step	Hyp	Ref	Expression
1		cnq 6264	. 2 class Q.
2		cnpi 6256	. . . 4 class N.
3	2, 2	cxp 4286	. . 3 class ( N. X. N.)
4		ceq 6263	. . 3 class ~Q
5	3, 4	cqs 6041	. 2 class (( N. X. N.) /. ~Q )
6	1, 5	wceq 1242	1 wff Q. = (( N. X. N.) /. ~Q )

This definition is referenced by:  nqex  6347  0nnq  6348  1nq  6350  addpipqqs  6354  mulpipqqs  6357  ordpipqqs  6358  addclnq  6359  mulclnq  6360  dmaddpqlem  6361  nqpi  6362  addcomnqg  6365  addassnqg  6366  mulcomnqg  6367  mulassnqg  6368  distrnqg  6371  mulidnq  6373  recexnq  6374  nqtri3or  6380  ltsonq  6382  ltanqg  6384  ltmnqg  6385  ltexnqq  6391  prarloclemarch  6401  prarloclemarch2  6402  nnnq  6405  nqnq0  6424  nqpnq0nq  6436  prarloclemlt  6476  prarloclemlo  6477  prarloclemcalc  6485  nqprm  6525