Definition df-nq 5038

Description: Define class of positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 5240, and is intended to be used only by the construction. From Proposition 9-2.2 of [Gleason] p. 117.

Assertion

Ref	Expression
df-nq	|- Q. = ((N. X. N.)/. ~Q )

Detailed syntax breakdown of Definition df-nq

Step	Hyp	Ref	Expression
1		cnq 4979	. 2 class Q.
2		cnpi 4972	. . . 4 class N.
3	2, 2	cxp 3168	. . 3 class (N. X. N.)
4		ceq 4978	. . 3 class ~Q
5	3, 4	cqs 4260	. 2 class ((N. X. N.)/. ~Q )
6	1, 5	wceq 956	1 wff Q. = ((N. X. N.)/. ~Q )

This definition is referenced by:  nqex 5049  0npq 5050  addpipq 5054  mulpipq 5055  ordpipq 5056  1q 5057  addclpq 5058  mulclpq 5060  addcompq 5062  addasspq 5063  mulcompq 5064  mulasspq 5065  distrpq 5067  mulidpq 5069  recmulpq 5070  ltsopq 5075  ltapq 5076  ltmpq 5077  ltexpq 5080  halfpq 5082  prlem934 5139

Copyright terms: Public domain