ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-nqqs Structured version   GIF version

Definition df-nqqs 6332
Description: Define class of positive fractions. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. From Proposition 9-2.2 of [Gleason] p. 117. (Contributed by NM, 16-Aug-1995.)
Assertion
Ref Expression
df-nqqs Q = ((N × N) / ~Q )

Detailed syntax breakdown of Definition df-nqqs
StepHypRef Expression
1 cnq 6264 . 2 class Q
2 cnpi 6256 . . . 4 class N
32, 2cxp 4286 . . 3 class (N × N)
4 ceq 6263 . . 3 class ~Q
53, 4cqs 6041 . 2 class ((N × N) / ~Q )
61, 5wceq 1242 1 wff Q = ((N × N) / ~Q )
Colors of variables: wff set class
This definition is referenced by:  nqex  6347  0nnq  6348  1nq  6350  addpipqqs  6354  mulpipqqs  6357  ordpipqqs  6358  addclnq  6359  mulclnq  6360  dmaddpqlem  6361  nqpi  6362  addcomnqg  6365  addassnqg  6366  mulcomnqg  6367  mulassnqg  6368  distrnqg  6371  mulidnq  6373  recexnq  6374  nqtri3or  6380  ltsonq  6382  ltanqg  6384  ltmnqg  6385  ltexnqq  6391  prarloclemarch  6401  prarloclemarch2  6402  nnnq  6405  nqnq0  6423  nqpnq0nq  6435  prarloclemlt  6475  prarloclemlo  6476  prarloclemcalc  6484  nqprm  6524
  Copyright terms: Public domain W3C validator