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

Definition df-nr 8869
Description: Define class of signed reals. This is a "temporary" set used in the construction of complex numbers df-c 8930, 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 8676 . 2  class  R.
2 cnp 8668 . . . 4  class  P.
32, 2cxp 4817 . . 3  class  ( P. 
X.  P. )
4 cer 8675 . . 3  class  ~R
53, 4cqs 6841 . 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  8884  mulsrpr  8885  ltsrpr  8886  0nsr  8888  0r  8889  1sr  8890  m1r  8891  addclsr  8892  mulclsr  8893  addcomsr  8896  addasssr  8897  mulcomsr  8898  mulasssr  8899  distrsr  8900  ltsosr  8903  0idsr  8906  1idsr  8907  00sr  8908  ltasr  8909  recexsrlem  8912  mulgt0sr  8914  map2psrpr  8919  axcnex  8956  wuncn  8979
  Copyright terms: Public domain W3C validator