Definition df-nqqs 7432

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 7364	. 2 class Q.
2		cnpi 7356	. . . 4 class N.
3	2, 2	cxp 4662	. . 3 class ( N. X. N. )
4		ceq 7363	. . 3 class ~Q
5	3, 4	cqs 6600	. 2 class ( ( N. X. N. ) /. ~Q )
6	1, 5	wceq 1364	1 wff Q. = ( ( N. X. N. ) /. ~Q )

This definition is referenced by:  nqex  7447  0nnq  7448  1nq  7450  addpipqqs  7454  mulpipqqs  7457  ordpipqqs  7458  addclnq  7459  mulclnq  7460  dmaddpqlem  7461  nqpi  7462  addcomnqg  7465  addassnqg  7466  mulcomnqg  7467  mulassnqg  7468  distrnqg  7471  mulidnq  7473  recexnq  7474  nqtri3or  7480  ltsonq  7482  ltanqg  7484  ltmnqg  7485  ltexnqq  7492  prarloclemarch  7502  prarloclemarch2  7503  nnnq  7506  nqnq0  7525  nqpnq0nq  7537  prarloclemlt  7577  prarloclemlo  7578  prarloclemcalc  7586  nqprm  7626