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

Definition df-nr 9227
Description: Define class of signed reals. This is a "temporary" set used in the construction of complex numbers df-c 9288, 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 9034 . 2  class  R.
2 cnp 9026 . . . 4  class  P.
32, 2cxp 4838 . . 3  class  ( P. 
X.  P. )
4 cer 9033 . . 3  class  ~R
53, 4cqs 7100 . 2  class  ( ( P.  X.  P. ) /.  ~R  )
61, 5wceq 1369 1  wff  R.  =  ( ( P.  X.  P. ) /.  ~R  )
Colors of variables: wff setvar class
This definition is referenced by:  addsrpr  9242  mulsrpr  9243  ltsrpr  9244  0nsr  9246  0r  9247  1sr  9248  m1r  9249  addclsr  9250  mulclsr  9251  addcomsr  9254  addasssr  9255  mulcomsr  9256  mulasssr  9257  distrsr  9258  ltsosr  9261  0idsr  9264  1idsr  9265  00sr  9266  ltasr  9267  recexsrlem  9270  mulgt0sr  9272  map2psrpr  9277  axcnex  9314  wuncn  9337
  Copyright terms: Public domain W3C validator