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

Definition df-nr 8615
Description: Define class of signed reals. This is a "temporary" set used in the construction of complex numbers df-c 8676, 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 8422 . 2  class  R.
2 cnp 8414 . . . 4  class  P.
32, 2cxp 4624 . . 3  class  ( P. 
X.  P. )
4 cer 8421 . . 3  class  ~R
53, 4cqs 6592 . 2  class  ( ( P.  X.  P. ) /.  ~R  )
61, 5wceq 1619 1  wff  R.  =  ( ( P.  X.  P. ) /.  ~R  )
Colors of variables: wff set class
This definition is referenced by:  addsrpr  8630  mulsrpr  8631  ltsrpr  8632  0nsr  8634  0r  8635  1sr  8636  m1r  8637  addclsr  8638  mulclsr  8639  addcomsr  8642  addasssr  8643  mulcomsr  8644  mulasssr  8645  distrsr  8646  ltsosr  8649  0idsr  8652  1idsr  8653  00sr  8654  ltasr  8655  recexsrlem  8658  mulgt0sr  8660  map2psrpr  8665  axcnex  8702  wuncn  8725
  Copyright terms: Public domain W3C validator