Definition df-nqqs 7679

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 7611	. 2 class Q.
2		cnpi 7603	. . . 4 class N.
3	2, 2	cxp 4752	. . 3 class ( N. X. N. )
4		ceq 7610	. . 3 class ~Q
5	3, 4	cqs 6779	. 2 class ( ( N. X. N. ) /. ~Q )
6	1, 5	wceq 1398	1 wff Q. = ( ( N. X. N. ) /. ~Q )

This definition is referenced by:  nqex  7694  0nnq  7695  1nq  7697  addpipqqs  7701  mulpipqqs  7704  ordpipqqs  7705  addclnq  7706  mulclnq  7707  dmaddpqlem  7708  nqpi  7709  addcomnqg  7712  addassnqg  7713  mulcomnqg  7714  mulassnqg  7715  distrnqg  7718  mulidnq  7720  recexnq  7721  nqtri3or  7727  ltsonq  7729  ltanqg  7731  ltmnqg  7732  ltexnqq  7739  prarloclemarch  7749  prarloclemarch2  7750  nnnq  7753  nqnq0  7772  nqpnq0nq  7784  prarloclemlt  7824  prarloclemlo  7825  prarloclemcalc  7833  nqprm  7873