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

Definition df-nqqs 6446
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 6378 . 2 class Q
2 cnpi 6370 . . . 4 class N
32, 2cxp 4343 . . 3 class (N × N)
4 ceq 6377 . . 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  6461  0nnq  6462  1nq  6464  addpipqqs  6468  mulpipqqs  6471  ordpipqqs  6472  addclnq  6473  mulclnq  6474  dmaddpqlem  6475  nqpi  6476  addcomnqg  6479  addassnqg  6480  mulcomnqg  6481  mulassnqg  6482  distrnqg  6485  mulidnq  6487  recexnq  6488  nqtri3or  6494  ltsonq  6496  ltanqg  6498  ltmnqg  6499  ltexnqq  6506  prarloclemarch  6516  prarloclemarch2  6517  nnnq  6520  nqnq0  6539  nqpnq0nq  6551  prarloclemlt  6591  prarloclemlo  6592  prarloclemcalc  6600  nqprm  6640
  Copyright terms: Public domain W3C validator