Definition df-nqqs 7310

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 7242	. 2 class Q.
2		cnpi 7234	. . . 4 class N.
3	2, 2	cxp 4609	. . 3 class ( N. X. N. )
4		ceq 7241	. . 3 class ~Q
5	3, 4	cqs 6512	. 2 class ( ( N. X. N. ) /. ~Q )
6	1, 5	wceq 1348	1 wff Q. = ( ( N. X. N. ) /. ~Q )

This definition is referenced by:  nqex  7325  0nnq  7326  1nq  7328  addpipqqs  7332  mulpipqqs  7335  ordpipqqs  7336  addclnq  7337  mulclnq  7338  dmaddpqlem  7339  nqpi  7340  addcomnqg  7343  addassnqg  7344  mulcomnqg  7345  mulassnqg  7346  distrnqg  7349  mulidnq  7351  recexnq  7352  nqtri3or  7358  ltsonq  7360  ltanqg  7362  ltmnqg  7363  ltexnqq  7370  prarloclemarch  7380  prarloclemarch2  7381  nnnq  7384  nqnq0  7403  nqpnq0nq  7415  prarloclemlt  7455  prarloclemlo  7456  prarloclemcalc  7464  nqprm  7504