Definition df-nqqs 7410

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 7342	. 2 class Q.
2		cnpi 7334	. . . 4 class N.
3	2, 2	cxp 4658	. . 3 class ( N. X. N. )
4		ceq 7341	. . 3 class ~Q
5	3, 4	cqs 6588	. 2 class ( ( N. X. N. ) /. ~Q )
6	1, 5	wceq 1364	1 wff Q. = ( ( N. X. N. ) /. ~Q )

This definition is referenced by:  nqex  7425  0nnq  7426  1nq  7428  addpipqqs  7432  mulpipqqs  7435  ordpipqqs  7436  addclnq  7437  mulclnq  7438  dmaddpqlem  7439  nqpi  7440  addcomnqg  7443  addassnqg  7444  mulcomnqg  7445  mulassnqg  7446  distrnqg  7449  mulidnq  7451  recexnq  7452  nqtri3or  7458  ltsonq  7460  ltanqg  7462  ltmnqg  7463  ltexnqq  7470  prarloclemarch  7480  prarloclemarch2  7481  nnnq  7484  nqnq0  7503  nqpnq0nq  7515  prarloclemlt  7555  prarloclemlo  7556  prarloclemcalc  7564  nqprm  7604