![]() |
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 6602 |
. 2
![]() ![]() | |
2 | cnpi 6594 |
. . . 4
![]() ![]() | |
3 | 2, 2 | cxp 4389 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() |
4 | ceq 6601 |
. . 3
![]() ![]() | |
5 | 3, 4 | cqs 6193 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 1, 5 | wceq 1285 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: nqex 6685 0nnq 6686 1nq 6688 addpipqqs 6692 mulpipqqs 6695 ordpipqqs 6696 addclnq 6697 mulclnq 6698 dmaddpqlem 6699 nqpi 6700 addcomnqg 6703 addassnqg 6704 mulcomnqg 6705 mulassnqg 6706 distrnqg 6709 mulidnq 6711 recexnq 6712 nqtri3or 6718 ltsonq 6720 ltanqg 6722 ltmnqg 6723 ltexnqq 6730 prarloclemarch 6740 prarloclemarch2 6741 nnnq 6744 nqnq0 6763 nqpnq0nq 6775 prarloclemlt 6815 prarloclemlo 6816 prarloclemcalc 6824 nqprm 6864 |
Copyright terms: Public domain | W3C validator |