![]() |
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 6741 | . 2 class Q | |
2 | cnpi 6733 | . . . 4 class N | |
3 | 2, 2 | cxp 4398 | . . 3 class (N × N) |
4 | ceq 6740 | . . 3 class ~Q | |
5 | 3, 4 | cqs 6220 | . 2 class ((N × N) / ~Q ) |
6 | 1, 5 | wceq 1285 | 1 wff Q = ((N × N) / ~Q ) |
Colors of variables: wff set class |
This definition is referenced by: nqex 6824 0nnq 6825 1nq 6827 addpipqqs 6831 mulpipqqs 6834 ordpipqqs 6835 addclnq 6836 mulclnq 6837 dmaddpqlem 6838 nqpi 6839 addcomnqg 6842 addassnqg 6843 mulcomnqg 6844 mulassnqg 6845 distrnqg 6848 mulidnq 6850 recexnq 6851 nqtri3or 6857 ltsonq 6859 ltanqg 6861 ltmnqg 6862 ltexnqq 6869 prarloclemarch 6879 prarloclemarch2 6880 nnnq 6883 nqnq0 6902 nqpnq0nq 6914 prarloclemlt 6954 prarloclemlo 6955 prarloclemcalc 6963 nqprm 7003 |
Copyright terms: Public domain | W3C validator |