![]() |
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 7309 | . 2 class Q | |
2 | cnpi 7301 | . . . 4 class N | |
3 | 2, 2 | cxp 4642 | . . 3 class (N × N) |
4 | ceq 7308 | . . 3 class ~Q | |
5 | 3, 4 | cqs 6558 | . 2 class ((N × N) / ~Q ) |
6 | 1, 5 | wceq 1364 | 1 wff Q = ((N × N) / ~Q ) |
Colors of variables: wff set class |
This definition is referenced by: nqex 7392 0nnq 7393 1nq 7395 addpipqqs 7399 mulpipqqs 7402 ordpipqqs 7403 addclnq 7404 mulclnq 7405 dmaddpqlem 7406 nqpi 7407 addcomnqg 7410 addassnqg 7411 mulcomnqg 7412 mulassnqg 7413 distrnqg 7416 mulidnq 7418 recexnq 7419 nqtri3or 7425 ltsonq 7427 ltanqg 7429 ltmnqg 7430 ltexnqq 7437 prarloclemarch 7447 prarloclemarch2 7448 nnnq 7451 nqnq0 7470 nqpnq0nq 7482 prarloclemlt 7522 prarloclemlo 7523 prarloclemcalc 7531 nqprm 7571 |
Copyright terms: Public domain | W3C validator |