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

Definition df-nqqs 6670
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 6602 . 2  class  Q.
2 cnpi 6594 . . . 4  class  N.
32, 2cxp 4389 . . 3  class  ( N. 
X.  N. )
4 ceq 6601 . . 3  class  ~Q
53, 4cqs 6193 . 2  class  ( ( N.  X.  N. ) /.  ~Q  )
61, 5wceq 1285 1  wff  Q.  =  ( ( N.  X.  N. ) /.  ~Q  )
Colors of variables: wff set class
This definition is referenced by:  nqex  6685  0nnq  6686  1nq  6688  addpipqqs  6692  mulpipqqs  6695  ordpipqqs  6696  addclnq  6697  mulclnq  6698  dmaddpqlem  6699  nqpi  6700  addcomnqg  6703  addassnqg  6704  mulcomnqg  6705  mulassnqg  6706  distrnqg  6709  mulidnq  6711  recexnq  6712  nqtri3or  6718  ltsonq  6720  ltanqg  6722  ltmnqg  6723  ltexnqq  6730  prarloclemarch  6740  prarloclemarch2  6741  nnnq  6744  nqnq0  6763  nqpnq0nq  6775  prarloclemlt  6815  prarloclemlo  6816  prarloclemcalc  6824  nqprm  6864
  Copyright terms: Public domain W3C validator