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

Definition df-nr 8684
Description: Define class of signed reals. This is a "temporary" set used in the construction of complex numbers df-c 8745, 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.  X.  P. ) /.  ~R  )

Detailed syntax breakdown of Definition df-nr
StepHypRef Expression
1 cnr 8491 . 2  class  R.
2 cnp 8483 . . . 4  class  P.
32, 2cxp 4689 . . 3  class  ( P. 
X.  P. )
4 cer 8490 . . 3  class  ~R
53, 4cqs 6661 . 2  class  ( ( P.  X.  P. ) /.  ~R  )
61, 5wceq 1625 1  wff  R.  =  ( ( P.  X.  P. ) /.  ~R  )
Colors of variables: wff set class
This definition is referenced by:  addsrpr  8699  mulsrpr  8700  ltsrpr  8701  0nsr  8703  0r  8704  1sr  8705  m1r  8706  addclsr  8707  mulclsr  8708  addcomsr  8711  addasssr  8712  mulcomsr  8713  mulasssr  8714  distrsr  8715  ltsosr  8718  0idsr  8721  1idsr  8722  00sr  8723  ltasr  8724  recexsrlem  8727  mulgt0sr  8729  map2psrpr  8734  axcnex  8771  wuncn  8794
  Copyright terms: Public domain W3C validator