Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-nqqs | Unicode 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 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cnq 6378 | . 2 | |
2 | cnpi 6370 | . . . 4 | |
3 | 2, 2 | cxp 4343 | . . 3 |
4 | ceq 6377 | . . 3 | |
5 | 3, 4 | cqs 6105 | . 2 |
6 | 1, 5 | wceq 1243 | 1 |
Colors of variables: wff set class |
This definition is referenced by: nqex 6461 0nnq 6462 1nq 6464 addpipqqs 6468 mulpipqqs 6471 ordpipqqs 6472 addclnq 6473 mulclnq 6474 dmaddpqlem 6475 nqpi 6476 addcomnqg 6479 addassnqg 6480 mulcomnqg 6481 mulassnqg 6482 distrnqg 6485 mulidnq 6487 recexnq 6488 nqtri3or 6494 ltsonq 6496 ltanqg 6498 ltmnqg 6499 ltexnqq 6506 prarloclemarch 6516 prarloclemarch2 6517 nnnq 6520 nqnq0 6539 nqpnq0nq 6551 prarloclemlt 6591 prarloclemlo 6592 prarloclemcalc 6600 nqprm 6640 |
Copyright terms: Public domain | W3C validator |