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

Definition df-nqqs 7346
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 7278 . 2  class  Q.
2 cnpi 7270 . . . 4  class  N.
32, 2cxp 4624 . . 3  class  ( N. 
X.  N. )
4 ceq 7277 . . 3  class  ~Q
53, 4cqs 6533 . 2  class  ( ( N.  X.  N. ) /.  ~Q  )
61, 5wceq 1353 1  wff  Q.  =  ( ( N.  X.  N. ) /.  ~Q  )
Colors of variables: wff set class
This definition is referenced by:  nqex  7361  0nnq  7362  1nq  7364  addpipqqs  7368  mulpipqqs  7371  ordpipqqs  7372  addclnq  7373  mulclnq  7374  dmaddpqlem  7375  nqpi  7376  addcomnqg  7379  addassnqg  7380  mulcomnqg  7381  mulassnqg  7382  distrnqg  7385  mulidnq  7387  recexnq  7388  nqtri3or  7394  ltsonq  7396  ltanqg  7398  ltmnqg  7399  ltexnqq  7406  prarloclemarch  7416  prarloclemarch2  7417  nnnq  7420  nqnq0  7439  nqpnq0nq  7451  prarloclemlt  7491  prarloclemlo  7492  prarloclemcalc  7500  nqprm  7540
  Copyright terms: Public domain W3C validator