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

Definition df-nr 6870
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 × P) / ~R )

Detailed syntax breakdown of Definition df-nr
StepHypRef Expression
1 cnr 6453 . 2 class R
2 cnp 6447 . . . 4 class P
32, 2cxp 4371 . . 3 class (P × P)
4 cer 6452 . . 3 class ~R
53, 4cqs 6136 . 2 class ((P × P) / ~R )
61, 5wceq 1259 1 wff R = ((P × P) / ~R )
Colors of variables: wff set class
This definition is referenced by:  addsrpr  6888  mulsrpr  6889  ltsrprg  6890  gt0srpr  6891  0nsr  6892  0r  6893  1sr  6894  m1r  6895  addclsr  6896  mulclsr  6897  addcomsrg  6898  addasssrg  6899  mulcomsrg  6900  mulasssrg  6901  distrsrg  6902  lttrsr  6905  ltposr  6906  ltsosr  6907  0idsr  6910  1idsr  6911  00sr  6912  ltasrg  6913  recexgt0sr  6916  mulgt0sr  6920  aptisr  6921  mulextsr1  6923  archsr  6924  srpospr  6925  prsrcl  6926  addvalex  6978  pitonnlem2  6981  pitore  6984  recnnre  6985  axcnex  6993
  Copyright terms: Public domain W3C validator