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

Definition df-nr 8895
Description: Define class of signed reals. This is a "temporary" set used in the construction of complex numbers df-c 8956, 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 8702 . 2  class  R.
2 cnp 8694 . . . 4  class  P.
32, 2cxp 4839 . . 3  class  ( P. 
X.  P. )
4 cer 8701 . . 3  class  ~R
53, 4cqs 6867 . 2  class  ( ( P.  X.  P. ) /.  ~R  )
61, 5wceq 1649 1  wff  R.  =  ( ( P.  X.  P. ) /.  ~R  )
Colors of variables: wff set class
This definition is referenced by:  addsrpr  8910  mulsrpr  8911  ltsrpr  8912  0nsr  8914  0r  8915  1sr  8916  m1r  8917  addclsr  8918  mulclsr  8919  addcomsr  8922  addasssr  8923  mulcomsr  8924  mulasssr  8925  distrsr  8926  ltsosr  8929  0idsr  8932  1idsr  8933  00sr  8934  ltasr  8935  recexsrlem  8938  mulgt0sr  8940  map2psrpr  8945  axcnex  8982  wuncn  9005
  Copyright terms: Public domain W3C validator