Definition df-nqqs 7705

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 7637	. 2 class Q.
2		cnpi 7629	. . . 4 class N.
3	2, 2	cxp 4767	. . 3 class ( N. X. N. )
4		ceq 7636	. . 3 class ~Q
5	3, 4	cqs 6796	. 2 class ( ( N. X. N. ) /. ~Q )
6	1, 5	wceq 1402	1 wff Q. = ( ( N. X. N. ) /. ~Q )

This definition is referenced by:  nqex  7720  0nnq  7721  1nq  7723  addpipqqs  7727  mulpipqqs  7730  ordpipqqs  7731  addclnq  7732  mulclnq  7733  dmaddpqlem  7734  nqpi  7735  addcomnqg  7738  addassnqg  7739  mulcomnqg  7740  mulassnqg  7741  distrnqg  7744  mulidnq  7746  recexnq  7747  nqtri3or  7753  ltsonq  7755  ltanqg  7757  ltmnqg  7758  ltexnqq  7765  prarloclemarch  7775  prarloclemarch2  7776  nnnq  7779  nqnq0  7798  nqpnq0nq  7810  prarloclemlt  7850  prarloclemlo  7851  prarloclemcalc  7859  nqprm  7899