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

Definition df-nqqs 6809
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 6741 . 2 class Q
2 cnpi 6733 . . . 4 class N
32, 2cxp 4398 . . 3 class (N × N)
4 ceq 6740 . . 3 class ~Q
53, 4cqs 6220 . 2 class ((N × N) / ~Q )
61, 5wceq 1285 1 wff Q = ((N × N) / ~Q )
Colors of variables: wff set class
This definition is referenced by:  nqex  6824  0nnq  6825  1nq  6827  addpipqqs  6831  mulpipqqs  6834  ordpipqqs  6835  addclnq  6836  mulclnq  6837  dmaddpqlem  6838  nqpi  6839  addcomnqg  6842  addassnqg  6843  mulcomnqg  6844  mulassnqg  6845  distrnqg  6848  mulidnq  6850  recexnq  6851  nqtri3or  6857  ltsonq  6859  ltanqg  6861  ltmnqg  6862  ltexnqq  6869  prarloclemarch  6879  prarloclemarch2  6880  nnnq  6883  nqnq0  6902  nqpnq0nq  6914  prarloclemlt  6954  prarloclemlo  6955  prarloclemcalc  6963  nqprm  7003
  Copyright terms: Public domain W3C validator