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 10531, 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 10275 | . 2 class R | |
2 | cnp 10269 | . . . 4 class P | |
3 | 2, 2 | cxp 5546 | . . 3 class (P × P) |
4 | cer 10274 | . . 3 class ~R | |
5 | 3, 4 | cqs 8277 | . 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 10474 addsrpr 10485 mulsrpr 10486 ltsrpr 10487 0nsr 10489 0r 10490 1sr 10491 m1r 10492 addclsr 10493 mulclsr 10494 addcomsr 10497 addasssr 10498 mulcomsr 10499 mulasssr 10500 distrsr 10501 ltsosr 10504 0idsr 10507 1idsr 10508 00sr 10509 ltasr 10510 recexsrlem 10513 mulgt0sr 10515 map2psrpr 10520 wuncn 10580 |
Copyright terms: Public domain | W3C validator |