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

Definition df-nr 9757
 Description: Define class of signed reals. This is a "temporary" set used in the construction of complex numbers df-c 9821, 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 9566 . 2 class R
2 cnp 9560 . . . 4 class P
32, 2cxp 5036 . . 3 class (P × P)
4 cer 9565 . . 3 class ~R
53, 4cqs 7628 . 2 class ((P × P) / ~R )
61, 5wceq 1475 1 wff R = ((P × P) / ~R )
 Colors of variables: wff setvar class This definition is referenced by:  addsrpr  9775  mulsrpr  9776  ltsrpr  9777  0nsr  9779  0r  9780  1sr  9781  m1r  9782  addclsr  9783  mulclsr  9784  addcomsr  9787  addasssr  9788  mulcomsr  9789  mulasssr  9790  distrsr  9791  ltsosr  9794  0idsr  9797  1idsr  9798  00sr  9799  ltasr  9800  recexsrlem  9803  mulgt0sr  9805  map2psrpr  9810  axcnex  9847  wuncn  9870
 Copyright terms: Public domain W3C validator