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

Definition df-nr 6810
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 6393 . 2 class R
2 cnp 6387 . . . 4 class P
32, 2cxp 4343 . . 3 class (P × P)
4 cer 6392 . . 3 class ~R
53, 4cqs 6105 . 2 class ((P × P) / ~R )
61, 5wceq 1243 1 wff R = ((P × P) / ~R )
Colors of variables: wff set class
This definition is referenced by:  addsrpr  6828  mulsrpr  6829  ltsrprg  6830  gt0srpr  6831  0nsr  6832  0r  6833  1sr  6834  m1r  6835  addclsr  6836  mulclsr  6837  addcomsrg  6838  addasssrg  6839  mulcomsrg  6840  mulasssrg  6841  distrsrg  6842  lttrsr  6845  ltposr  6846  ltsosr  6847  0idsr  6850  1idsr  6851  00sr  6852  ltasrg  6853  recexgt0sr  6856  mulgt0sr  6860  aptisr  6861  mulextsr1  6863  archsr  6864  srpospr  6865  prsrcl  6866  addvalex  6918  pitonnlem2  6921  pitore  6924  recnnre  6925  axcnex  6933
  Copyright terms: Public domain W3C validator