MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-nr Structured version   Visualization version   GIF version

Definition df-nr 9731
Description: Define class of signed reals. This is a "temporary" set used in the construction of complex numbers df-c 9795, 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.)
Assertion
Ref Expression
df-nr R = ((P × P) / ~R )

Detailed syntax breakdown of Definition df-nr
StepHypRef Expression
1 cnr 9540 . 2 class R
2 cnp 9534 . . . 4 class P
32, 2cxp 5023 . . 3 class (P × P)
4 cer 9539 . . 3 class ~R
53, 4cqs 7602 . 2 class ((P × P) / ~R )
61, 5wceq 1474 1 wff R = ((P × P) / ~R )
Colors of variables: wff setvar class
This definition is referenced by:  addsrpr  9749  mulsrpr  9750  ltsrpr  9751  0nsr  9753  0r  9754  1sr  9755  m1r  9756  addclsr  9757  mulclsr  9758  addcomsr  9761  addasssr  9762  mulcomsr  9763  mulasssr  9764  distrsr  9765  ltsosr  9768  0idsr  9771  1idsr  9772  00sr  9773  ltasr  9774  recexsrlem  9777  mulgt0sr  9779  map2psrpr  9784  axcnex  9821  wuncn  9844
  Copyright terms: Public domain W3C validator