Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-nr | GIF version |
Description: Define class of signed reals. 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-4.2 of [Gleason] p. 126. (Contributed by NM, 25-Jul-1995.) |
Ref | Expression |
---|---|
df-nr | ⊢ R = ((P × P) / ~R ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cnr 6487 | . 2 class R | |
2 | cnp 6481 | . . . 4 class P | |
3 | 2, 2 | cxp 4361 | . . 3 class (P × P) |
4 | cer 6486 | . . 3 class ~R | |
5 | 3, 4 | cqs 6128 | . 2 class ((P × P) / ~R ) |
6 | 1, 5 | wceq 1284 | 1 wff R = ((P × P) / ~R ) |
Colors of variables: wff set class |
This definition is referenced by: addsrpr 6922 mulsrpr 6923 ltsrprg 6924 gt0srpr 6925 0nsr 6926 0r 6927 1sr 6928 m1r 6929 addclsr 6930 mulclsr 6931 addcomsrg 6932 addasssrg 6933 mulcomsrg 6934 mulasssrg 6935 distrsrg 6936 lttrsr 6939 ltposr 6940 ltsosr 6941 0idsr 6944 1idsr 6945 00sr 6946 ltasrg 6947 recexgt0sr 6950 mulgt0sr 6954 aptisr 6955 mulextsr1 6957 archsr 6958 srpospr 6959 prsrcl 6960 addvalex 7012 pitonnlem2 7015 pitore 7018 recnnre 7019 axcnex 7027 |
Copyright terms: Public domain | W3C validator |