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 10160
Description: Define class of signed reals. This is a "temporary" set used in the construction of complex numbers df-c 10224, 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 9969 . 2 class R
2 cnp 9963 . . . 4 class P
32, 2cxp 5306 . . 3 class (P × P)
4 cer 9968 . . 3 class ~R
53, 4cqs 7975 . 2 class ((P × P) / ~R )
61, 5wceq 1637 1 wff R = ((P × P) / ~R )
Colors of variables: wff setvar class
This definition is referenced by:  addsrpr  10178  mulsrpr  10179  ltsrpr  10180  0nsr  10182  0r  10183  1sr  10184  m1r  10185  addclsr  10186  mulclsr  10187  addcomsr  10190  addasssr  10191  mulcomsr  10192  mulasssr  10193  distrsr  10194  ltsosr  10197  0idsr  10200  1idsr  10201  00sr  10202  ltasr  10203  recexsrlem  10206  mulgt0sr  10208  map2psrpr  10213  axcnex  10250  wuncn  10273
  Copyright terms: Public domain W3C validator