Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-nqqs | GIF version |
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.) |
Ref | Expression |
---|---|
df-nqqs | ⊢ Q = ((N × N) / ~Q ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cnq 7056 | . 2 class Q | |
2 | cnpi 7048 | . . . 4 class N | |
3 | 2, 2 | cxp 4507 | . . 3 class (N × N) |
4 | ceq 7055 | . . 3 class ~Q | |
5 | 3, 4 | cqs 6396 | . 2 class ((N × N) / ~Q ) |
6 | 1, 5 | wceq 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 |