Definition df-nqqs 7715

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 7647	. 2 class Q.
2		cnpi 7639	. . . 4 class N.
3	2, 2	cxp 4772	. . 3 class ( N. X. N. )
4		ceq 7646	. . 3 class ~Q
5	3, 4	cqs 6806	. 2 class ( ( N. X. N. ) /. ~Q )
6	1, 5	wceq 1402	1 wff Q. = ( ( N. X. N. ) /. ~Q )

This definition is used by:  nqex  7730  0nnq  7731  1nq  7733  addpipqqs  7737  mulpipqqs  7740  ordpipqqs  7741  addclnq  7742  mulclnq  7743  dmaddpqlem  7744  nqpi  7745  addcomnqg  7748  addassnqg  7749  mulcomnqg  7750  mulassnqg  7751  distrnqg  7754  mulidnq  7756  recexnq  7757  nqtri3or  7763  ltsonq  7765  ltanqg  7767  ltmnqg  7768  ltexnqq  7775  prarloclemarch  7785  prarloclemarch2  7786  nnnq  7789  nqnq0  7808  nqpnq0nq  7820  prarloclemlt  7860  prarloclemlo  7861  prarloclemcalc  7869  nqprm  7909