Definition df-nq 5235

Description: Define class of positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 5437, 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 5176	. 2 class Q.
2		cnpi 5169	. . . 4 class N.
3	2, 2	cxp 3289	. . 3 class (N. X. N.)
4		ceq 5175	. . 3 class ~Q
5	3, 4	cqs 4443	. 2 class ((N. X. N.)/. ~Q )
6	1, 5	wceq 1018	1 wff Q. = ((N. X. N.)/. ~Q )

This definition is referenced by:  nqex 5246  0npq 5247  addpipq 5251  mulpipq 5252  ordpipq 5253  1q 5254  addclpq 5255  mulclpq 5257  addcompq 5259  addasspq 5260  mulcompq 5261  mulasspq 5262  distrpq 5264  mulidpq 5266  recmulpq 5267  ltsopq 5272  ltapq 5273  ltmpq 5274  ltexpq 5277  halfpq 5279  prlem934 5336

Copyright terms: Public domain