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 6470 | . 2 class Q | |
2 | cnpi 6462 | . . . 4 class N | |
3 | 2, 2 | cxp 4361 | . . 3 class (N × N) |
4 | ceq 6469 | . . 3 class ~Q | |
5 | 3, 4 | cqs 6128 | . 2 class ((N × N) / ~Q ) |
6 | 1, 5 | wceq 1284 | 1 wff Q = ((N × N) / ~Q ) |
Colors of variables: wff set class |
This definition is referenced by: nqex 6553 0nnq 6554 1nq 6556 addpipqqs 6560 mulpipqqs 6563 ordpipqqs 6564 addclnq 6565 mulclnq 6566 dmaddpqlem 6567 nqpi 6568 addcomnqg 6571 addassnqg 6572 mulcomnqg 6573 mulassnqg 6574 distrnqg 6577 mulidnq 6579 recexnq 6580 nqtri3or 6586 ltsonq 6588 ltanqg 6590 ltmnqg 6591 ltexnqq 6598 prarloclemarch 6608 prarloclemarch2 6609 nnnq 6612 nqnq0 6631 nqpnq0nq 6643 prarloclemlt 6683 prarloclemlo 6684 prarloclemcalc 6692 nqprm 6732 |
Copyright terms: Public domain | W3C validator |