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 11093
Description: Define class of signed reals. This is a "temporary" set used in the construction of complex numbers df-c 11158, 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 10902 . 2 class R
2 cnp 10896 . . . 4 class P
32, 2cxp 5686 . . 3 class (P × P)
4 cer 10901 . . 3 class ~R
53, 4cqs 8742 . 2 class ((P × P) / ~R )
61, 5wceq 1536 1 wff R = ((P × P) / ~R )
Colors of variables: wff setvar class
This definition is referenced by:  nrex1  11101  addsrpr  11112  mulsrpr  11113  ltsrpr  11114  0nsr  11116  0r  11117  1sr  11118  m1r  11119  addclsr  11120  mulclsr  11121  addcomsr  11124  addasssr  11125  mulcomsr  11126  mulasssr  11127  distrsr  11128  ltsosr  11131  0idsr  11134  1idsr  11135  00sr  11136  ltasr  11137  recexsrlem  11140  mulgt0sr  11142  map2psrpr  11147  wuncn  11207
  Copyright terms: Public domain W3C validator