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

Definition df-nr 8861
Description: Define class of signed reals. This is a "temporary" set used in the construction of complex numbers df-c 8922, 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 8668 . 2  class  R.
2 cnp 8660 . . . 4  class  P.
32, 2cxp 4809 . . 3  class  ( P. 
X.  P. )
4 cer 8667 . . 3  class  ~R
53, 4cqs 6833 . 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  8876  mulsrpr  8877  ltsrpr  8878  0nsr  8880  0r  8881  1sr  8882  m1r  8883  addclsr  8884  mulclsr  8885  addcomsr  8888  addasssr  8889  mulcomsr  8890  mulasssr  8891  distrsr  8892  ltsosr  8895  0idsr  8898  1idsr  8899  00sr  8900  ltasr  8901  recexsrlem  8904  mulgt0sr  8906  map2psrpr  8911  axcnex  8948  wuncn  8971
  Copyright terms: Public domain W3C validator