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

Definition df-nqqs 6968
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 6900 . 2 class Q
2 cnpi 6892 . . . 4 class N
32, 2cxp 4450 . . 3 class (N × N)
4 ceq 6899 . . 3 class ~Q
53, 4cqs 6305 . 2 class ((N × N) / ~Q )
61, 5wceq 1290 1 wff Q = ((N × N) / ~Q )
Colors of variables: wff set class
This definition is referenced by:  nqex  6983  0nnq  6984  1nq  6986  addpipqqs  6990  mulpipqqs  6993  ordpipqqs  6994  addclnq  6995  mulclnq  6996  dmaddpqlem  6997  nqpi  6998  addcomnqg  7001  addassnqg  7002  mulcomnqg  7003  mulassnqg  7004  distrnqg  7007  mulidnq  7009  recexnq  7010  nqtri3or  7016  ltsonq  7018  ltanqg  7020  ltmnqg  7021  ltexnqq  7028  prarloclemarch  7038  prarloclemarch2  7039  nnnq  7042  nqnq0  7061  nqpnq0nq  7073  prarloclemlt  7113  prarloclemlo  7114  prarloclemcalc  7122  nqprm  7162
  Copyright terms: Public domain W3C validator