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

Definition df-nr 7464
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 7047 . 2  class  R.
2 cnp 7041 . . . 4  class  P.
32, 2cxp 4495 . . 3  class  ( P. 
X.  P. )
4 cer 7046 . . 3  class  ~R
53, 4cqs 6380 . 2  class  ( ( P.  X.  P. ) /.  ~R  )
61, 5wceq 1312 1  wff  R.  =  ( ( P.  X.  P. ) /.  ~R  )
Colors of variables: wff set class
This definition is referenced by:  addsrpr  7482  mulsrpr  7483  ltsrprg  7484  gt0srpr  7485  0nsr  7486  0r  7487  1sr  7488  m1r  7489  addclsr  7490  mulclsr  7491  addcomsrg  7492  addasssrg  7493  mulcomsrg  7494  mulasssrg  7495  distrsrg  7496  lttrsr  7499  ltposr  7500  ltsosr  7501  0idsr  7504  1idsr  7505  00sr  7506  ltasrg  7507  recexgt0sr  7510  mulgt0sr  7514  aptisr  7515  mulextsr1  7517  archsr  7518  srpospr  7519  prsrcl  7520  addvalex  7573  pitonnlem2  7576  pitore  7579  recnnre  7580  axcnex  7588
  Copyright terms: Public domain W3C validator