Definition df-nq 5050

Description: Define class of positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 5252, 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 4991	. 2 class Q.
2		cnpi 4984	. . . 4 class N.
3	2, 2	cxp 3174	. . 3 class (N. X. N.)
4		ceq 4990	. . 3 class ~Q
5	3, 4	cqs 4266	. 2 class ((N. X. N.)/. ~Q )
6	1, 5	wceq 958	1 wff Q. = ((N. X. N.)/. ~Q )

This definition is referenced by:  nqex 5061  0npq 5062  addpipq 5066  mulpipq 5067  ordpipq 5068  1q 5069  addclpq 5070  mulclpq 5072  addcompq 5074  addasspq 5075  mulcompq 5076  mulasspq 5077  distrpq 5079  mulidpq 5081  recmulpq 5082  ltsopq 5087  ltapq 5088  ltmpq 5089  ltexpq 5092  halfpq 5094  prlem934 5151

Copyright terms: Public domain