| 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 11161, 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 10905 | . 2 class R | |
| 2 | cnp 10899 | . . . 4 class P | |
| 3 | 2, 2 | cxp 5683 | . . 3 class (P × P) |
| 4 | cer 10904 | . . 3 class ~R | |
| 5 | 3, 4 | cqs 8744 | . 2 class ((P × P) / ~R ) |
| 6 | 1, 5 | wceq 1540 | 1 wff R = ((P × P) / ~R ) |
| Colors of variables: wff setvar class |
| This definition is referenced by: nrex1 11104 addsrpr 11115 mulsrpr 11116 ltsrpr 11117 0nsr 11119 0r 11120 1sr 11121 m1r 11122 addclsr 11123 mulclsr 11124 addcomsr 11127 addasssr 11128 mulcomsr 11129 mulasssr 11130 distrsr 11131 ltsosr 11134 0idsr 11137 1idsr 11138 00sr 11139 ltasr 11140 recexsrlem 11143 mulgt0sr 11145 map2psrpr 11150 wuncn 11210 |
| Copyright terms: Public domain | W3C validator |