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

Definition df-nr 9481
Description: Define class of signed reals. This is a "temporary" set used in the construction of complex numbers df-c 9545, 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 9290 . 2  class  R.
2 cnp 9284 . . . 4  class  P.
32, 2cxp 4847 . . 3  class  ( P. 
X.  P. )
4 cer 9289 . . 3  class  ~R
53, 4cqs 7366 . 2  class  ( ( P.  X.  P. ) /.  ~R  )
61, 5wceq 1437 1  wff  R.  =  ( ( P.  X.  P. ) /.  ~R  )
Colors of variables: wff setvar class
This definition is referenced by:  addsrpr  9499  mulsrpr  9500  ltsrpr  9501  0nsr  9503  0r  9504  1sr  9505  m1r  9506  addclsr  9507  mulclsr  9508  addcomsr  9511  addasssr  9512  mulcomsr  9513  mulasssr  9514  distrsr  9515  ltsosr  9518  0idsr  9521  1idsr  9522  00sr  9523  ltasr  9524  recexsrlem  9527  mulgt0sr  9529  map2psrpr  9534  axcnex  9571  wuncn  9594
  Copyright terms: Public domain W3C validator