Definition df-nqqs 6670

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 6602	. 2 class Q.
2		cnpi 6594	. . . 4 class N.
3	2, 2	cxp 4389	. . 3 class ( N. X. N. )
4		ceq 6601	. . 3 class ~Q
5	3, 4	cqs 6193	. 2 class ( ( N. X. N. ) /. ~Q )
6	1, 5	wceq 1285	1 wff Q. = ( ( N. X. N. ) /. ~Q )

This definition is referenced by:  nqex  6685  0nnq  6686  1nq  6688  addpipqqs  6692  mulpipqqs  6695  ordpipqqs  6696  addclnq  6697  mulclnq  6698  dmaddpqlem  6699  nqpi  6700  addcomnqg  6703  addassnqg  6704  mulcomnqg  6705  mulassnqg  6706  distrnqg  6709  mulidnq  6711  recexnq  6712  nqtri3or  6718  ltsonq  6720  ltanqg  6722  ltmnqg  6723  ltexnqq  6730  prarloclemarch  6740  prarloclemarch2  6741  nnnq  6744  nqnq0  6763  nqpnq0nq  6775  prarloclemlt  6815  prarloclemlo  6816  prarloclemcalc  6824  nqprm  6864