Definition df-nqqs 7558

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 7490	. 2 class Q.
2		cnpi 7482	. . . 4 class N.
3	2, 2	cxp 4721	. . 3 class ( N. X. N. )
4		ceq 7489	. . 3 class ~Q
5	3, 4	cqs 6696	. 2 class ( ( N. X. N. ) /. ~Q )
6	1, 5	wceq 1395	1 wff Q. = ( ( N. X. N. ) /. ~Q )

This definition is referenced by:  nqex  7573  0nnq  7574  1nq  7576  addpipqqs  7580  mulpipqqs  7583  ordpipqqs  7584  addclnq  7585  mulclnq  7586  dmaddpqlem  7587  nqpi  7588  addcomnqg  7591  addassnqg  7592  mulcomnqg  7593  mulassnqg  7594  distrnqg  7597  mulidnq  7599  recexnq  7600  nqtri3or  7606  ltsonq  7608  ltanqg  7610  ltmnqg  7611  ltexnqq  7618  prarloclemarch  7628  prarloclemarch2  7629  nnnq  7632  nqnq0  7651  nqpnq0nq  7663  prarloclemlt  7703  prarloclemlo  7704  prarloclemcalc  7712  nqprm  7752