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

Definition df-nqqs 6503
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 6435 . 2  class  Q.
2 cnpi 6427 . . . 4  class  N.
32, 2cxp 4370 . . 3  class  ( N. 
X.  N. )
4 ceq 6434 . . 3  class  ~Q
53, 4cqs 6135 . 2  class  ( ( N.  X.  N. ) /.  ~Q  )
61, 5wceq 1259 1  wff  Q.  =  ( ( N.  X.  N. ) /.  ~Q  )
Colors of variables: wff set class
This definition is referenced by:  nqex  6518  0nnq  6519  1nq  6521  addpipqqs  6525  mulpipqqs  6528  ordpipqqs  6529  addclnq  6530  mulclnq  6531  dmaddpqlem  6532  nqpi  6533  addcomnqg  6536  addassnqg  6537  mulcomnqg  6538  mulassnqg  6539  distrnqg  6542  mulidnq  6544  recexnq  6545  nqtri3or  6551  ltsonq  6553  ltanqg  6555  ltmnqg  6556  ltexnqq  6563  prarloclemarch  6573  prarloclemarch2  6574  nnnq  6577  nqnq0  6596  nqpnq0nq  6608  prarloclemlt  6648  prarloclemlo  6649  prarloclemcalc  6657  nqprm  6697
  Copyright terms: Public domain W3C validator