Definition df-nq 5010

Description: Define class of positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 5212, 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 4951	. 2 class Q.
2		cnpi 4944	. . . 4 class N.
3	2, 2	cxp 3158	. . 3 class (N. X. N.)
4		ceq 4950	. . 3 class ~Q
5	3, 4	cqs 4244	. 2 class ((N. X. N.)/. ~Q )
6	1, 5	wceq 953	1 wff Q. = ((N. X. N.)/. ~Q )

This definition is referenced by:  nqex 5021  0npq 5022  addpipq 5026  mulpipq 5027  ordpipq 5028  1q 5029  addclpq 5030  mulclpq 5032  addcompq 5034  addasspq 5035  mulcompq 5036  mulasspq 5037  distrpq 5039  mulidpq 5041  recmulpq 5042  ltsopq 5047  ltapq 5048  ltmpq 5049  ltexpq 5052  halfpq 5054  prlem934 5111

Copyright terms: Public domain