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 10670
Description: Define class of signed reals. This is a "temporary" set used in the construction of complex numbers df-c 10735, 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 10479 . 2 class R
2 cnp 10473 . . . 4 class P
32, 2cxp 5549 . . 3 class (P × P)
4 cer 10478 . . 3 class ~R
53, 4cqs 8390 . 2 class ((P × P) / ~R )
61, 5wceq 1543 1 wff R = ((P × P) / ~R )
Colors of variables: wff setvar class
This definition is referenced by:  nrex1  10678  addsrpr  10689  mulsrpr  10690  ltsrpr  10691  0nsr  10693  0r  10694  1sr  10695  m1r  10696  addclsr  10697  mulclsr  10698  addcomsr  10701  addasssr  10702  mulcomsr  10703  mulasssr  10704  distrsr  10705  ltsosr  10708  0idsr  10711  1idsr  10712  00sr  10713  ltasr  10714  recexsrlem  10717  mulgt0sr  10719  map2psrpr  10724  wuncn  10784
  Copyright terms: Public domain W3C validator