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

Definition df-nr 8682
Description: Define class of signed reals. This is a "temporary" set used in the construction of complex numbers df-c 8743, 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 8489 . 2  class  R.
2 cnp 8481 . . . 4  class  P.
32, 2cxp 4687 . . 3  class  ( P. 
X.  P. )
4 cer 8488 . . 3  class  ~R
53, 4cqs 6659 . 2  class  ( ( P.  X.  P. ) /.  ~R  )
61, 5wceq 1623 1  wff  R.  =  ( ( P.  X.  P. ) /.  ~R  )
Colors of variables: wff set class
This definition is referenced by:  addsrpr  8697  mulsrpr  8698  ltsrpr  8699  0nsr  8701  0r  8702  1sr  8703  m1r  8704  addclsr  8705  mulclsr  8706  addcomsr  8709  addasssr  8710  mulcomsr  8711  mulasssr  8712  distrsr  8713  ltsosr  8716  0idsr  8719  1idsr  8720  00sr  8721  ltasr  8722  recexsrlem  8725  mulgt0sr  8727  map2psrpr  8732  axcnex  8769  wuncn  8792
  Copyright terms: Public domain W3C validator