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

Definition df-nr 9432
Description: Define class of signed reals. This is a "temporary" set used in the construction of complex numbers df-c 9496, 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 9241 . 2  class  R.
2 cnp 9235 . . . 4  class  P.
32, 2cxp 4983 . . 3  class  ( P. 
X.  P. )
4 cer 9240 . . 3  class  ~R
53, 4cqs 7308 . 2  class  ( ( P.  X.  P. ) /.  ~R  )
61, 5wceq 1381 1  wff  R.  =  ( ( P.  X.  P. ) /.  ~R  )
Colors of variables: wff setvar class
This definition is referenced by:  addsrpr  9450  mulsrpr  9451  ltsrpr  9452  0nsr  9454  0r  9455  1sr  9456  m1r  9457  addclsr  9458  mulclsr  9459  addcomsr  9462  addasssr  9463  mulcomsr  9464  mulasssr  9465  distrsr  9466  ltsosr  9469  0idsr  9472  1idsr  9473  00sr  9474  ltasr  9475  recexsrlem  9478  mulgt0sr  9480  map2psrpr  9485  axcnex  9522  wuncn  9545
  Copyright terms: Public domain W3C validator