Definition df-nqqs 7289

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 7221	. 2 class Q.
2		cnpi 7213	. . . 4 class N.
3	2, 2	cxp 4602	. . 3 class ( N. X. N. )
4		ceq 7220	. . 3 class ~Q
5	3, 4	cqs 6500	. 2 class ( ( N. X. N. ) /. ~Q )
6	1, 5	wceq 1343	1 wff Q. = ( ( N. X. N. ) /. ~Q )

This definition is referenced by:  nqex  7304  0nnq  7305  1nq  7307  addpipqqs  7311  mulpipqqs  7314  ordpipqqs  7315  addclnq  7316  mulclnq  7317  dmaddpqlem  7318  nqpi  7319  addcomnqg  7322  addassnqg  7323  mulcomnqg  7324  mulassnqg  7325  distrnqg  7328  mulidnq  7330  recexnq  7331  nqtri3or  7337  ltsonq  7339  ltanqg  7341  ltmnqg  7342  ltexnqq  7349  prarloclemarch  7359  prarloclemarch2  7360  nnnq  7363  nqnq0  7382  nqpnq0nq  7394  prarloclemlt  7434  prarloclemlo  7435  prarloclemcalc  7443  nqprm  7483