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 7212 | . 2 class Q | |
2 | cnpi 7204 | . . . 4 class N | |
3 | 2, 2 | cxp 4596 | . . 3 class (N × N) |
4 | ceq 7211 | . . 3 class ~Q | |
5 | 3, 4 | cqs 6491 | . 2 class ((N × N) / ~Q ) |
6 | 1, 5 | wceq 1342 | 1 wff Q = ((N × N) / ~Q ) |
Colors of variables: wff set class |
This definition is referenced by: nqex 7295 0nnq 7296 1nq 7298 addpipqqs 7302 mulpipqqs 7305 ordpipqqs 7306 addclnq 7307 mulclnq 7308 dmaddpqlem 7309 nqpi 7310 addcomnqg 7313 addassnqg 7314 mulcomnqg 7315 mulassnqg 7316 distrnqg 7319 mulidnq 7321 recexnq 7322 nqtri3or 7328 ltsonq 7330 ltanqg 7332 ltmnqg 7333 ltexnqq 7340 prarloclemarch 7350 prarloclemarch2 7351 nnnq 7354 nqnq0 7373 nqpnq0nq 7385 prarloclemlt 7425 prarloclemlo 7426 prarloclemcalc 7434 nqprm 7474 |
Copyright terms: Public domain | W3C validator |