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

Definition df-nqqs 6851
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 6783 . 2  class  Q.
2 cnpi 6775 . . . 4  class  N.
32, 2cxp 4409 . . 3  class  ( N. 
X.  N. )
4 ceq 6782 . . 3  class  ~Q
53, 4cqs 6243 . 2  class  ( ( N.  X.  N. ) /.  ~Q  )
61, 5wceq 1287 1  wff  Q.  =  ( ( N.  X.  N. ) /.  ~Q  )
Colors of variables: wff set class
This definition is referenced by:  nqex  6866  0nnq  6867  1nq  6869  addpipqqs  6873  mulpipqqs  6876  ordpipqqs  6877  addclnq  6878  mulclnq  6879  dmaddpqlem  6880  nqpi  6881  addcomnqg  6884  addassnqg  6885  mulcomnqg  6886  mulassnqg  6887  distrnqg  6890  mulidnq  6892  recexnq  6893  nqtri3or  6899  ltsonq  6901  ltanqg  6903  ltmnqg  6904  ltexnqq  6911  prarloclemarch  6921  prarloclemarch2  6922  nnnq  6925  nqnq0  6944  nqpnq0nq  6956  prarloclemlt  6996  prarloclemlo  6997  prarloclemcalc  7005  nqprm  7045
  Copyright terms: Public domain W3C validator