ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-nr Unicode version

Definition df-nr 7043
Description: Define class of signed reals. This is a "temporary" set used in the construction of complex numbers, 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.)
Assertion
Ref Expression
df-nr  |-  R.  =  ( ( P.  X.  P. ) /.  ~R  )

Detailed syntax breakdown of Definition df-nr
StepHypRef Expression
1 cnr 6626 . 2  class  R.
2 cnp 6620 . . . 4  class  P.
32, 2cxp 4390 . . 3  class  ( P. 
X.  P. )
4 cer 6625 . . 3  class  ~R
53, 4cqs 6194 . 2  class  ( ( P.  X.  P. ) /.  ~R  )
61, 5wceq 1285 1  wff  R.  =  ( ( P.  X.  P. ) /.  ~R  )
Colors of variables: wff set class
This definition is referenced by:  addsrpr  7061  mulsrpr  7062  ltsrprg  7063  gt0srpr  7064  0nsr  7065  0r  7066  1sr  7067  m1r  7068  addclsr  7069  mulclsr  7070  addcomsrg  7071  addasssrg  7072  mulcomsrg  7073  mulasssrg  7074  distrsrg  7075  lttrsr  7078  ltposr  7079  ltsosr  7080  0idsr  7083  1idsr  7084  00sr  7085  ltasrg  7086  recexgt0sr  7089  mulgt0sr  7093  aptisr  7094  mulextsr1  7096  archsr  7097  srpospr  7098  prsrcl  7099  addvalex  7151  pitonnlem2  7154  pitore  7157  recnnre  7158  axcnex  7166
  Copyright terms: Public domain W3C validator