MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-nr Structured version   Visualization version   GIF version

Definition df-nr 10324
Description: Define class of signed reals. This is a "temporary" set used in the construction of complex numbers df-c 10389, 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.) (New usage is discouraged.)
Assertion
Ref Expression
df-nr R = ((P × P) / ~R )

Detailed syntax breakdown of Definition df-nr
StepHypRef Expression
1 cnr 10133 . 2 class R
2 cnp 10127 . . . 4 class P
32, 2cxp 5441 . . 3 class (P × P)
4 cer 10132 . . 3 class ~R
53, 4cqs 8138 . 2 class ((P × P) / ~R )
61, 5wceq 1522 1 wff R = ((P × P) / ~R )
Colors of variables: wff setvar class
This definition is referenced by:  nrex1  10332  addsrpr  10343  mulsrpr  10344  ltsrpr  10345  0nsr  10347  0r  10348  1sr  10349  m1r  10350  addclsr  10351  mulclsr  10352  addcomsr  10355  addasssr  10356  mulcomsr  10357  mulasssr  10358  distrsr  10359  ltsosr  10362  0idsr  10365  1idsr  10366  00sr  10367  ltasr  10368  recexsrlem  10371  mulgt0sr  10373  map2psrpr  10378  wuncn  10438
  Copyright terms: Public domain W3C validator