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

Definition df-nqqs 7120
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 7052 . 2  class  Q.
2 cnpi 7044 . . . 4  class  N.
32, 2cxp 4505 . . 3  class  ( N. 
X.  N. )
4 ceq 7051 . . 3  class  ~Q
53, 4cqs 6394 . 2  class  ( ( N.  X.  N. ) /.  ~Q  )
61, 5wceq 1314 1  wff  Q.  =  ( ( N.  X.  N. ) /.  ~Q  )
Colors of variables: wff set class
This definition is referenced by:  nqex  7135  0nnq  7136  1nq  7138  addpipqqs  7142  mulpipqqs  7145  ordpipqqs  7146  addclnq  7147  mulclnq  7148  dmaddpqlem  7149  nqpi  7150  addcomnqg  7153  addassnqg  7154  mulcomnqg  7155  mulassnqg  7156  distrnqg  7159  mulidnq  7161  recexnq  7162  nqtri3or  7168  ltsonq  7170  ltanqg  7172  ltmnqg  7173  ltexnqq  7180  prarloclemarch  7190  prarloclemarch2  7191  nnnq  7194  nqnq0  7213  nqpnq0nq  7225  prarloclemlt  7265  prarloclemlo  7266  prarloclemcalc  7274  nqprm  7314
  Copyright terms: Public domain W3C validator