![]() |
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 7278 |
. 2
![]() ![]() | |
2 | cnpi 7270 |
. . . 4
![]() ![]() | |
3 | 2, 2 | cxp 4624 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() |
4 | ceq 7277 |
. . 3
![]() ![]() | |
5 | 3, 4 | cqs 6533 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 1, 5 | wceq 1353 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: nqex 7361 0nnq 7362 1nq 7364 addpipqqs 7368 mulpipqqs 7371 ordpipqqs 7372 addclnq 7373 mulclnq 7374 dmaddpqlem 7375 nqpi 7376 addcomnqg 7379 addassnqg 7380 mulcomnqg 7381 mulassnqg 7382 distrnqg 7385 mulidnq 7387 recexnq 7388 nqtri3or 7394 ltsonq 7396 ltanqg 7398 ltmnqg 7399 ltexnqq 7406 prarloclemarch 7416 prarloclemarch2 7417 nnnq 7420 nqnq0 7439 nqpnq0nq 7451 prarloclemlt 7491 prarloclemlo 7492 prarloclemcalc 7500 nqprm 7540 |
Copyright terms: Public domain | W3C validator |