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

Definition df-nr 8927
Description: Define class of signed reals. This is a "temporary" set used in the construction of complex numbers df-c 8988, 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 8734 . 2  class  R.
2 cnp 8726 . . . 4  class  P.
32, 2cxp 4868 . . 3  class  ( P. 
X.  P. )
4 cer 8733 . . 3  class  ~R
53, 4cqs 6896 . 2  class  ( ( P.  X.  P. ) /.  ~R  )
61, 5wceq 1652 1  wff  R.  =  ( ( P.  X.  P. ) /.  ~R  )
Colors of variables: wff set class
This definition is referenced by:  addsrpr  8942  mulsrpr  8943  ltsrpr  8944  0nsr  8946  0r  8947  1sr  8948  m1r  8949  addclsr  8950  mulclsr  8951  addcomsr  8954  addasssr  8955  mulcomsr  8956  mulasssr  8957  distrsr  8958  ltsosr  8961  0idsr  8964  1idsr  8965  00sr  8966  ltasr  8967  recexsrlem  8970  mulgt0sr  8972  map2psrpr  8977  axcnex  9014  wuncn  9037
  Copyright terms: Public domain W3C validator