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

Definition df-nqqs 6444
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 6376 . 2 class Q
2 cnpi 6368 . . . 4 class N
32, 2cxp 4343 . . 3 class (N × N)
4 ceq 6375 . . 3 class ~Q
53, 4cqs 6105 . 2 class ((N × N) / ~Q )
61, 5wceq 1243 1 wff Q = ((N × N) / ~Q )
Colors of variables: wff set class
This definition is referenced by:  nqex  6459  0nnq  6460  1nq  6462  addpipqqs  6466  mulpipqqs  6469  ordpipqqs  6470  addclnq  6471  mulclnq  6472  dmaddpqlem  6473  nqpi  6474  addcomnqg  6477  addassnqg  6478  mulcomnqg  6479  mulassnqg  6480  distrnqg  6483  mulidnq  6485  recexnq  6486  nqtri3or  6492  ltsonq  6494  ltanqg  6496  ltmnqg  6497  ltexnqq  6504  prarloclemarch  6514  prarloclemarch2  6515  nnnq  6518  nqnq0  6537  nqpnq0nq  6549  prarloclemlt  6589  prarloclemlo  6590  prarloclemcalc  6598  nqprm  6638
  Copyright terms: Public domain W3C validator