Definition df-nqqs 7415

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 7347	. 2 class Q.
2		cnpi 7339	. . . 4 class N.
3	2, 2	cxp 4661	. . 3 class ( N. X. N. )
4		ceq 7346	. . 3 class ~Q
5	3, 4	cqs 6591	. 2 class ( ( N. X. N. ) /. ~Q )
6	1, 5	wceq 1364	1 wff Q. = ( ( N. X. N. ) /. ~Q )

This definition is referenced by:  nqex  7430  0nnq  7431  1nq  7433  addpipqqs  7437  mulpipqqs  7440  ordpipqqs  7441  addclnq  7442  mulclnq  7443  dmaddpqlem  7444  nqpi  7445  addcomnqg  7448  addassnqg  7449  mulcomnqg  7450  mulassnqg  7451  distrnqg  7454  mulidnq  7456  recexnq  7457  nqtri3or  7463  ltsonq  7465  ltanqg  7467  ltmnqg  7468  ltexnqq  7475  prarloclemarch  7485  prarloclemarch2  7486  nnnq  7489  nqnq0  7508  nqpnq0nq  7520  prarloclemlt  7560  prarloclemlo  7561  prarloclemcalc  7569  nqprm  7609