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

Definition df-nr 8562
Description: Define class of signed reals. This is a "temporary" set used in the construction of complex numbers df-c 8623, 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 8369 . 2  class  R.
2 cnp 8361 . . . 4  class  P.
32, 2cxp 4578 . . 3  class  ( P. 
X.  P. )
4 cer 8368 . . 3  class  ~R
53, 4cqs 6545 . 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  8577  mulsrpr  8578  ltsrpr  8579  0nsr  8581  0r  8582  1sr  8583  m1r  8584  addclsr  8585  mulclsr  8586  addcomsr  8589  addasssr  8590  mulcomsr  8591  mulasssr  8592  distrsr  8593  ltsosr  8596  0idsr  8599  1idsr  8600  00sr  8601  ltasr  8602  recexsrlem  8605  mulgt0sr  8607  map2psrpr  8612  axcnex  8649  wuncn  8672
  Copyright terms: Public domain W3C validator