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

Definition df-nqqs 6325
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 6257 . 2 class Q
2 cnpi 6249 . . . 4 class N
32, 2cxp 4285 . . 3 class (N × N)
4 ceq 6256 . . 3 class ~Q
53, 4cqs 6034 . 2 class ((N × N) / ~Q )
61, 5wceq 1242 1 wff Q = ((N × N) / ~Q )
Colors of variables: wff set class
This definition is referenced by:  nqex  6340  0nnq  6341  1nq  6343  addpipqqs  6347  mulpipqqs  6350  ordpipqqs  6351  addclnq  6352  mulclnq  6353  dmaddpqlem  6354  nqpi  6355  addcomnqg  6358  addassnqg  6359  mulcomnqg  6360  mulassnqg  6361  distrnqg  6364  mulidnq  6366  recexnq  6367  nqtri3or  6373  ltsonq  6375  ltanqg  6377  ltmnqg  6378  ltexnqq  6384  prarloclemarch  6394  prarloclemarch2  6395  nnnq  6398  nqnq0  6416  nqpnq0nq  6428  prarloclemlt  6468  prarloclemlo  6469  prarloclemcalc  6477  nqprm  6518
  Copyright terms: Public domain W3C validator