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

Definition df-nqqs 7200
 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 × N) / ~Q )

Detailed syntax breakdown of Definition df-nqqs
StepHypRef Expression
1 cnq 7132 . 2 class Q
2 cnpi 7124 . . . 4 class N
32, 2cxp 4546 . . 3 class (N × N)
4 ceq 7131 . . 3 class ~Q
53, 4cqs 6437 . 2 class ((N × N) / ~Q )
61, 5wceq 1332 1 wff Q = ((N × N) / ~Q )
 Colors of variables: wff set class This definition is referenced by:  nqex  7215  0nnq  7216  1nq  7218  addpipqqs  7222  mulpipqqs  7225  ordpipqqs  7226  addclnq  7227  mulclnq  7228  dmaddpqlem  7229  nqpi  7230  addcomnqg  7233  addassnqg  7234  mulcomnqg  7235  mulassnqg  7236  distrnqg  7239  mulidnq  7241  recexnq  7242  nqtri3or  7248  ltsonq  7250  ltanqg  7252  ltmnqg  7253  ltexnqq  7260  prarloclemarch  7270  prarloclemarch2  7271  nnnq  7274  nqnq0  7293  nqpnq0nq  7305  prarloclemlt  7345  prarloclemlo  7346  prarloclemcalc  7354  nqprm  7394
 Copyright terms: Public domain W3C validator