Definition df-nq 3832

Description: Define class of positive fractions. This is a "temporary" set used in the construction of complex numbers df-c 4034, 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 × N) / ~Q )

Detailed syntax breakdown of Definition df-nq

Step	Hyp	Ref	Expression
1		cnq 3773	. 2 class Q
2		cnpi 3766	. . . 4 class N
3	2, 2	cxp 2408	. . 3 class (N × N)
4		ceq 3772	. . 3 class ~Q
5	3, 4	cqs 3199	. 2 class ((N × N) / ~Q )
6	1, 5	wceq 1091	1 wff Q = ((N × N) / ~Q )

This definition is referenced by:  nqex 3843  0npq 3844  addpipq 3848  mulpipq 3849  ordpipq 3850  1q 3851  addclpq 3852  mulclpq 3854  addcompq 3856  addasspq 3857  mulcompq 3858  mulasspq 3859  distrpq 3861  mulidpq 3863  recmulpq 3864  ltsopq 3869  ltapq 3870  ltmpq 3871  ltexpq 3874  halfpq 3876  prlem934 3933

metamath.org