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 11081
Description: Define class of signed reals. This is a "temporary" set used in the construction of complex numbers df-c 11146, 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 10890 . 2 class R
2 cnp 10884 . . . 4 class P
32, 2cxp 5676 . . 3 class (P × P)
4 cer 10889 . . 3 class ~R
53, 4cqs 8724 . 2 class ((P × P) / ~R )
61, 5wceq 1533 1 wff R = ((P × P) / ~R )
Colors of variables: wff setvar class
This definition is referenced by:  nrex1  11089  addsrpr  11100  mulsrpr  11101  ltsrpr  11102  0nsr  11104  0r  11105  1sr  11106  m1r  11107  addclsr  11108  mulclsr  11109  addcomsr  11112  addasssr  11113  mulcomsr  11114  mulasssr  11115  distrsr  11116  ltsosr  11119  0idsr  11122  1idsr  11123  00sr  11124  ltasr  11125  recexsrlem  11128  mulgt0sr  11130  map2psrpr  11135  wuncn  11195
  Copyright terms: Public domain W3C validator