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

Definition df-nqqs 6418
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.  X.  N. ) /.  ~Q  )

Detailed syntax breakdown of Definition df-nqqs
StepHypRef Expression
1 cnq 6350 . 2  class  Q.
2 cnpi 6342 . . . 4  class  N.
32, 2cxp 4321 . . 3  class  ( N. 
X.  N. )
4 ceq 6349 . . 3  class  ~Q
53, 4cqs 6083 . 2  class  ( ( N.  X.  N. ) /.  ~Q  )
61, 5wceq 1243 1  wff  Q.  =  ( ( N.  X.  N. ) /.  ~Q  )
Colors of variables: wff set class
This definition is referenced by:  nqex  6433  0nnq  6434  1nq  6436  addpipqqs  6440  mulpipqqs  6443  ordpipqqs  6444  addclnq  6445  mulclnq  6446  dmaddpqlem  6447  nqpi  6448  addcomnqg  6451  addassnqg  6452  mulcomnqg  6453  mulassnqg  6454  distrnqg  6457  mulidnq  6459  recexnq  6460  nqtri3or  6466  ltsonq  6468  ltanqg  6470  ltmnqg  6471  ltexnqq  6478  prarloclemarch  6488  prarloclemarch2  6489  nnnq  6492  nqnq0  6511  nqpnq0nq  6523  prarloclemlt  6563  prarloclemlo  6564  prarloclemcalc  6572  nqprm  6612
  Copyright terms: Public domain W3C validator