![]() |
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 10389, 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 10133 | . 2 class R | |
2 | cnp 10127 | . . . 4 class P | |
3 | 2, 2 | cxp 5441 | . . 3 class (P × P) |
4 | cer 10132 | . . 3 class ~R | |
5 | 3, 4 | cqs 8138 | . 2 class ((P × P) / ~R ) |
6 | 1, 5 | wceq 1522 | 1 wff R = ((P × P) / ~R ) |
Colors of variables: wff setvar class |
This definition is referenced by: nrex1 10332 addsrpr 10343 mulsrpr 10344 ltsrpr 10345 0nsr 10347 0r 10348 1sr 10349 m1r 10350 addclsr 10351 mulclsr 10352 addcomsr 10355 addasssr 10356 mulcomsr 10357 mulasssr 10358 distrsr 10359 ltsosr 10362 0idsr 10365 1idsr 10366 00sr 10367 ltasr 10368 recexsrlem 10371 mulgt0sr 10373 map2psrpr 10378 wuncn 10438 |
Copyright terms: Public domain | W3C validator |