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

Definition df-nr 8678
Description: Define class of signed reals. This is a "temporary" set used in the construction of complex numbers df-c 8739, 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 8485 . 2  class  R.
2 cnp 8477 . . . 4  class  P.
32, 2cxp 4686 . . 3  class  ( P. 
X.  P. )
4 cer 8484 . . 3  class  ~R
53, 4cqs 6655 . 2  class  ( ( P.  X.  P. ) /.  ~R  )
61, 5wceq 1623 1  wff  R.  =  ( ( P.  X.  P. ) /.  ~R  )
Colors of variables: wff set class
This definition is referenced by:  addsrpr  8693  mulsrpr  8694  ltsrpr  8695  0nsr  8697  0r  8698  1sr  8699  m1r  8700  addclsr  8701  mulclsr  8702  addcomsr  8705  addasssr  8706  mulcomsr  8707  mulasssr  8708  distrsr  8709  ltsosr  8712  0idsr  8715  1idsr  8716  00sr  8717  ltasr  8718  recexsrlem  8721  mulgt0sr  8723  map2psrpr  8728  axcnex  8765  wuncn  8788
  Copyright terms: Public domain W3C validator