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

Definition df-nr 7725
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 7295 . 2 class R
2 cnp 7289 . . . 4 class P
32, 2cxp 4624 . . 3 class (P × P)
4 cer 7294 . . 3 class ~R
53, 4cqs 6533 . 2 class ((P × P) / ~R )
61, 5wceq 1353 1 wff R = ((P × P) / ~R )
Colors of variables: wff set class
This definition is referenced by:  addsrpr  7743  mulsrpr  7744  ltsrprg  7745  gt0srpr  7746  0nsr  7747  0r  7748  1sr  7749  m1r  7750  addclsr  7751  mulclsr  7752  addcomsrg  7753  addasssrg  7754  mulcomsrg  7755  mulasssrg  7756  distrsrg  7757  lttrsr  7760  ltposr  7761  ltsosr  7762  0idsr  7765  1idsr  7766  00sr  7767  ltasrg  7768  recexgt0sr  7771  mulgt0sr  7776  aptisr  7777  mulextsr1  7779  archsr  7780  srpospr  7781  prsrcl  7782  ltpsrprg  7801  mappsrprg  7802  map2psrprg  7803  suplocsrlemb  7804  addvalex  7842  pitonnlem2  7845  pitore  7848  recnnre  7849  axcnex  7857
  Copyright terms: Public domain W3C validator