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

Definition df-nr 6869
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 6452 . 2  class  R.
2 cnp 6446 . . . 4  class  P.
32, 2cxp 4370 . . 3  class  ( P. 
X.  P. )
4 cer 6451 . . 3  class  ~R
53, 4cqs 6135 . 2  class  ( ( P.  X.  P. ) /.  ~R  )
61, 5wceq 1259 1  wff  R.  =  ( ( P.  X.  P. ) /.  ~R  )
Colors of variables: wff set class
This definition is referenced by:  addsrpr  6887  mulsrpr  6888  ltsrprg  6889  gt0srpr  6890  0nsr  6891  0r  6892  1sr  6893  m1r  6894  addclsr  6895  mulclsr  6896  addcomsrg  6897  addasssrg  6898  mulcomsrg  6899  mulasssrg  6900  distrsrg  6901  lttrsr  6904  ltposr  6905  ltsosr  6906  0idsr  6909  1idsr  6910  00sr  6911  ltasrg  6912  recexgt0sr  6915  mulgt0sr  6919  aptisr  6920  mulextsr1  6922  archsr  6923  srpospr  6924  prsrcl  6925  addvalex  6977  pitonnlem2  6980  pitore  6983  recnnre  6984  axcnex  6992
  Copyright terms: Public domain W3C validator