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

Definition df-nqqs 7377
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 7309 . 2 class Q
2 cnpi 7301 . . . 4 class N
32, 2cxp 4642 . . 3 class (N × N)
4 ceq 7308 . . 3 class ~Q
53, 4cqs 6558 . 2 class ((N × N) / ~Q )
61, 5wceq 1364 1 wff Q = ((N × N) / ~Q )
Colors of variables: wff set class
This definition is referenced by:  nqex  7392  0nnq  7393  1nq  7395  addpipqqs  7399  mulpipqqs  7402  ordpipqqs  7403  addclnq  7404  mulclnq  7405  dmaddpqlem  7406  nqpi  7407  addcomnqg  7410  addassnqg  7411  mulcomnqg  7412  mulassnqg  7413  distrnqg  7416  mulidnq  7418  recexnq  7419  nqtri3or  7425  ltsonq  7427  ltanqg  7429  ltmnqg  7430  ltexnqq  7437  prarloclemarch  7447  prarloclemarch2  7448  nnnq  7451  nqnq0  7470  nqpnq0nq  7482  prarloclemlt  7522  prarloclemlo  7523  prarloclemcalc  7531  nqprm  7571
  Copyright terms: Public domain W3C validator