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

Definition df-nr 7503
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 7073 . 2 class R
2 cnp 7067 . . . 4 class P
32, 2cxp 4507 . . 3 class (P × P)
4 cer 7072 . . 3 class ~R
53, 4cqs 6396 . 2 class ((P × P) / ~R )
61, 5wceq 1316 1 wff R = ((P × P) / ~R )
Colors of variables: wff set class
This definition is referenced by:  addsrpr  7521  mulsrpr  7522  ltsrprg  7523  gt0srpr  7524  0nsr  7525  0r  7526  1sr  7527  m1r  7528  addclsr  7529  mulclsr  7530  addcomsrg  7531  addasssrg  7532  mulcomsrg  7533  mulasssrg  7534  distrsrg  7535  lttrsr  7538  ltposr  7539  ltsosr  7540  0idsr  7543  1idsr  7544  00sr  7545  ltasrg  7546  recexgt0sr  7549  mulgt0sr  7554  aptisr  7555  mulextsr1  7557  archsr  7558  srpospr  7559  prsrcl  7560  ltpsrprg  7579  mappsrprg  7580  map2psrprg  7581  suplocsrlemb  7582  addvalex  7620  pitonnlem2  7623  pitore  7626  recnnre  7627  axcnex  7635
  Copyright terms: Public domain W3C validator