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

Definition df-nr 8650
Description: Define class of signed reals. This is a "temporary" set used in the construction of complex numbers df-c 8711, 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 8457 . 2  class  R.
2 cnp 8449 . . . 4  class  P.
32, 2cxp 4659 . . 3  class  ( P. 
X.  P. )
4 cer 8456 . . 3  class  ~R
53, 4cqs 6627 . 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  8665  mulsrpr  8666  ltsrpr  8667  0nsr  8669  0r  8670  1sr  8671  m1r  8672  addclsr  8673  mulclsr  8674  addcomsr  8677  addasssr  8678  mulcomsr  8679  mulasssr  8680  distrsr  8681  ltsosr  8684  0idsr  8687  1idsr  8688  00sr  8689  ltasr  8690  recexsrlem  8693  mulgt0sr  8695  map2psrpr  8700  axcnex  8737  wuncn  8760
  Copyright terms: Public domain W3C validator