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

Definition df-nr 7217
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 6800 . 2 class R
2 cnp 6794 . . . 4 class P
32, 2cxp 4409 . . 3 class (P × P)
4 cer 6799 . . 3 class ~R
53, 4cqs 6243 . 2 class ((P × P) / ~R )
61, 5wceq 1287 1 wff R = ((P × P) / ~R )
Colors of variables: wff set class
This definition is referenced by:  addsrpr  7235  mulsrpr  7236  ltsrprg  7237  gt0srpr  7238  0nsr  7239  0r  7240  1sr  7241  m1r  7242  addclsr  7243  mulclsr  7244  addcomsrg  7245  addasssrg  7246  mulcomsrg  7247  mulasssrg  7248  distrsrg  7249  lttrsr  7252  ltposr  7253  ltsosr  7254  0idsr  7257  1idsr  7258  00sr  7259  ltasrg  7260  recexgt0sr  7263  mulgt0sr  7267  aptisr  7268  mulextsr1  7270  archsr  7271  srpospr  7272  prsrcl  7273  addvalex  7325  pitonnlem2  7328  pitore  7331  recnnre  7332  axcnex  7340
  Copyright terms: Public domain W3C validator