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

Definition df-nqqs 7124
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 7056 . 2 class Q
2 cnpi 7048 . . . 4 class N
32, 2cxp 4507 . . 3 class (N × N)
4 ceq 7055 . . 3 class ~Q
53, 4cqs 6396 . 2 class ((N × N) / ~Q )
61, 5wceq 1316 1 wff Q = ((N × N) / ~Q )
Colors of variables: wff set class
This definition is referenced by:  nqex  7139  0nnq  7140  1nq  7142  addpipqqs  7146  mulpipqqs  7149  ordpipqqs  7150  addclnq  7151  mulclnq  7152  dmaddpqlem  7153  nqpi  7154  addcomnqg  7157  addassnqg  7158  mulcomnqg  7159  mulassnqg  7160  distrnqg  7163  mulidnq  7165  recexnq  7166  nqtri3or  7172  ltsonq  7174  ltanqg  7176  ltmnqg  7177  ltexnqq  7184  prarloclemarch  7194  prarloclemarch2  7195  nnnq  7198  nqnq0  7217  nqpnq0nq  7229  prarloclemlt  7269  prarloclemlo  7270  prarloclemcalc  7278  nqprm  7318
  Copyright terms: Public domain W3C validator