Definition df-nqqs 7346

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 7278	. 2 class Q.
2		cnpi 7270	. . . 4 class N.
3	2, 2	cxp 4624	. . 3 class ( N. X. N. )
4		ceq 7277	. . 3 class ~Q
5	3, 4	cqs 6533	. 2 class ( ( N. X. N. ) /. ~Q )
6	1, 5	wceq 1353	1 wff Q. = ( ( N. X. N. ) /. ~Q )

This definition is referenced by:  nqex  7361  0nnq  7362  1nq  7364  addpipqqs  7368  mulpipqqs  7371  ordpipqqs  7372  addclnq  7373  mulclnq  7374  dmaddpqlem  7375  nqpi  7376  addcomnqg  7379  addassnqg  7380  mulcomnqg  7381  mulassnqg  7382  distrnqg  7385  mulidnq  7387  recexnq  7388  nqtri3or  7394  ltsonq  7396  ltanqg  7398  ltmnqg  7399  ltexnqq  7406  prarloclemarch  7416  prarloclemarch2  7417  nnnq  7420  nqnq0  7439  nqpnq0nq  7451  prarloclemlt  7491  prarloclemlo  7492  prarloclemcalc  7500  nqprm  7540