![]() |
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 11158, 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 10902 | . 2 class R | |
2 | cnp 10896 | . . . 4 class P | |
3 | 2, 2 | cxp 5686 | . . 3 class (P × P) |
4 | cer 10901 | . . 3 class ~R | |
5 | 3, 4 | cqs 8742 | . 2 class ((P × P) / ~R ) |
6 | 1, 5 | wceq 1536 | 1 wff R = ((P × P) / ~R ) |
Colors of variables: wff setvar class |
This definition is referenced by: nrex1 11101 addsrpr 11112 mulsrpr 11113 ltsrpr 11114 0nsr 11116 0r 11117 1sr 11118 m1r 11119 addclsr 11120 mulclsr 11121 addcomsr 11124 addasssr 11125 mulcomsr 11126 mulasssr 11127 distrsr 11128 ltsosr 11131 0idsr 11134 1idsr 11135 00sr 11136 ltasr 11137 recexsrlem 11140 mulgt0sr 11142 map2psrpr 11147 wuncn 11207 |
Copyright terms: Public domain | W3C validator |