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 10532, 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 10276 | . 2 class R | |
2 | cnp 10270 | . . . 4 class P | |
3 | 2, 2 | cxp 5547 | . . 3 class (P × P) |
4 | cer 10275 | . . 3 class ~R | |
5 | 3, 4 | cqs 8278 | . 2 class ((P × P) / ~R ) |
6 | 1, 5 | wceq 1528 | 1 wff R = ((P × P) / ~R ) |
Colors of variables: wff setvar class |
This definition is referenced by: nrex1 10475 addsrpr 10486 mulsrpr 10487 ltsrpr 10488 0nsr 10490 0r 10491 1sr 10492 m1r 10493 addclsr 10494 mulclsr 10495 addcomsr 10498 addasssr 10499 mulcomsr 10500 mulasssr 10501 distrsr 10502 ltsosr 10505 0idsr 10508 1idsr 10509 00sr 10510 ltasr 10511 recexsrlem 10514 mulgt0sr 10516 map2psrpr 10521 wuncn 10581 |
Copyright terms: Public domain | W3C validator |