![]() |
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 6264 |
. 2
![]() ![]() | |
2 | cnpi 6256 |
. . . 4
![]() ![]() | |
3 | 2, 2 | cxp 4286 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() |
4 | ceq 6263 |
. . 3
![]() ![]() | |
5 | 3, 4 | cqs 6041 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 1, 5 | wceq 1242 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: nqex 6347 0nnq 6348 1nq 6350 addpipqqs 6354 mulpipqqs 6357 ordpipqqs 6358 addclnq 6359 mulclnq 6360 dmaddpqlem 6361 nqpi 6362 addcomnqg 6365 addassnqg 6366 mulcomnqg 6367 mulassnqg 6368 distrnqg 6371 mulidnq 6373 recexnq 6374 nqtri3or 6380 ltsonq 6382 ltanqg 6384 ltmnqg 6385 ltexnqq 6391 prarloclemarch 6401 prarloclemarch2 6402 nnnq 6405 nqnq0 6424 nqpnq0nq 6436 prarloclemlt 6476 prarloclemlo 6477 prarloclemcalc 6485 nqprm 6525 |
Copyright terms: Public domain | W3C validator |