Definition df-nqqs 6446

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 6378	. 2 class Q.
2		cnpi 6370	. . . 4 class N.
3	2, 2	cxp 4343	. . 3 class ( N. X. N. )
4		ceq 6377	. . 3 class ~Q
5	3, 4	cqs 6105	. 2 class ( ( N. X. N. ) /. ~Q )
6	1, 5	wceq 1243	1 wff Q. = ( ( N. X. N. ) /. ~Q )

This definition is referenced by:  nqex  6461  0nnq  6462  1nq  6464  addpipqqs  6468  mulpipqqs  6471  ordpipqqs  6472  addclnq  6473  mulclnq  6474  dmaddpqlem  6475  nqpi  6476  addcomnqg  6479  addassnqg  6480  mulcomnqg  6481  mulassnqg  6482  distrnqg  6485  mulidnq  6487  recexnq  6488  nqtri3or  6494  ltsonq  6496  ltanqg  6498  ltmnqg  6499  ltexnqq  6506  prarloclemarch  6516  prarloclemarch2  6517  nnnq  6520  nqnq0  6539  nqpnq0nq  6551  prarloclemlt  6591  prarloclemlo  6592  prarloclemcalc  6600  nqprm  6640