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

Definition df-nr 7647
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 7217 . 2 class R
2 cnp 7211 . . . 4 class P
32, 2cxp 4584 . . 3 class (P × P)
4 cer 7216 . . 3 class ~R
53, 4cqs 6479 . 2 class ((P × P) / ~R )
61, 5wceq 1335 1 wff R = ((P × P) / ~R )
Colors of variables: wff set class
This definition is referenced by:  addsrpr  7665  mulsrpr  7666  ltsrprg  7667  gt0srpr  7668  0nsr  7669  0r  7670  1sr  7671  m1r  7672  addclsr  7673  mulclsr  7674  addcomsrg  7675  addasssrg  7676  mulcomsrg  7677  mulasssrg  7678  distrsrg  7679  lttrsr  7682  ltposr  7683  ltsosr  7684  0idsr  7687  1idsr  7688  00sr  7689  ltasrg  7690  recexgt0sr  7693  mulgt0sr  7698  aptisr  7699  mulextsr1  7701  archsr  7702  srpospr  7703  prsrcl  7704  ltpsrprg  7723  mappsrprg  7724  map2psrprg  7725  suplocsrlemb  7726  addvalex  7764  pitonnlem2  7767  pitore  7770  recnnre  7771  axcnex  7779
  Copyright terms: Public domain W3C validator