![]() |
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 6900 | . 2 class Q | |
2 | cnpi 6892 | . . . 4 class N | |
3 | 2, 2 | cxp 4450 | . . 3 class (N × N) |
4 | ceq 6899 | . . 3 class ~Q | |
5 | 3, 4 | cqs 6305 | . 2 class ((N × N) / ~Q ) |
6 | 1, 5 | wceq 1290 | 1 wff Q = ((N × N) / ~Q ) |
Colors of variables: wff set class |
This definition is referenced by: nqex 6983 0nnq 6984 1nq 6986 addpipqqs 6990 mulpipqqs 6993 ordpipqqs 6994 addclnq 6995 mulclnq 6996 dmaddpqlem 6997 nqpi 6998 addcomnqg 7001 addassnqg 7002 mulcomnqg 7003 mulassnqg 7004 distrnqg 7007 mulidnq 7009 recexnq 7010 nqtri3or 7016 ltsonq 7018 ltanqg 7020 ltmnqg 7021 ltexnqq 7028 prarloclemarch 7038 prarloclemarch2 7039 nnnq 7042 nqnq0 7061 nqpnq0nq 7073 prarloclemlt 7113 prarloclemlo 7114 prarloclemcalc 7122 nqprm 7162 |
Copyright terms: Public domain | W3C validator |