![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-nr | Structured version Visualization version GIF version |
Description: Define class of signed reals. This is a "temporary" set used in the construction of complex numbers df-c 11146, 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.) (New usage is discouraged.) |
Ref | Expression |
---|---|
df-nr | ⊢ R = ((P × P) / ~R ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cnr 10890 | . 2 class R | |
2 | cnp 10884 | . . . 4 class P | |
3 | 2, 2 | cxp 5676 | . . 3 class (P × P) |
4 | cer 10889 | . . 3 class ~R | |
5 | 3, 4 | cqs 8724 | . 2 class ((P × P) / ~R ) |
6 | 1, 5 | wceq 1533 | 1 wff R = ((P × P) / ~R ) |
Colors of variables: wff setvar class |
This definition is referenced by: nrex1 11089 addsrpr 11100 mulsrpr 11101 ltsrpr 11102 0nsr 11104 0r 11105 1sr 11106 m1r 11107 addclsr 11108 mulclsr 11109 addcomsr 11112 addasssr 11113 mulcomsr 11114 mulasssr 11115 distrsr 11116 ltsosr 11119 0idsr 11122 1idsr 11123 00sr 11124 ltasr 11125 recexsrlem 11128 mulgt0sr 11130 map2psrpr 11135 wuncn 11195 |
Copyright terms: Public domain | W3C validator |