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

Definition df-nr 9423
Description: Define class of signed reals. This is a "temporary" set used in the construction of complex numbers df-c 9487, 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 9232 . 2  class  R.
2 cnp 9226 . . . 4  class  P.
32, 2cxp 4986 . . 3  class  ( P. 
X.  P. )
4 cer 9231 . . 3  class  ~R
53, 4cqs 7302 . 2  class  ( ( P.  X.  P. ) /.  ~R  )
61, 5wceq 1398 1  wff  R.  =  ( ( P.  X.  P. ) /.  ~R  )
Colors of variables: wff setvar class
This definition is referenced by:  addsrpr  9441  mulsrpr  9442  ltsrpr  9443  0nsr  9445  0r  9446  1sr  9447  m1r  9448  addclsr  9449  mulclsr  9450  addcomsr  9453  addasssr  9454  mulcomsr  9455  mulasssr  9456  distrsr  9457  ltsosr  9460  0idsr  9463  1idsr  9464  00sr  9465  ltasr  9466  recexsrlem  9469  mulgt0sr  9471  map2psrpr  9476  axcnex  9513  wuncn  9536
  Copyright terms: Public domain W3C validator