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 11096
Description: Define class of signed reals. This is a "temporary" set used in the construction of complex numbers df-c 11161, 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 10905 . 2 class R
2 cnp 10899 . . . 4 class P
32, 2cxp 5683 . . 3 class (P × P)
4 cer 10904 . . 3 class ~R
53, 4cqs 8744 . 2 class ((P × P) / ~R )
61, 5wceq 1540 1 wff R = ((P × P) / ~R )
Colors of variables: wff setvar class
This definition is referenced by:  nrex1  11104  addsrpr  11115  mulsrpr  11116  ltsrpr  11117  0nsr  11119  0r  11120  1sr  11121  m1r  11122  addclsr  11123  mulclsr  11124  addcomsr  11127  addasssr  11128  mulcomsr  11129  mulasssr  11130  distrsr  11131  ltsosr  11134  0idsr  11137  1idsr  11138  00sr  11139  ltasr  11140  recexsrlem  11143  mulgt0sr  11145  map2psrpr  11150  wuncn  11210
  Copyright terms: Public domain W3C validator