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 10466
Description: Define class of signed reals. This is a "temporary" set used in the construction of complex numbers df-c 10531, 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 10275 . 2 class R
2 cnp 10269 . . . 4 class P
32, 2cxp 5546 . . 3 class (P × P)
4 cer 10274 . . 3 class ~R
53, 4cqs 8277 . 2 class ((P × P) / ~R )
61, 5wceq 1528 1 wff R = ((P × P) / ~R )
Colors of variables: wff setvar class
This definition is referenced by:  nrex1  10474  addsrpr  10485  mulsrpr  10486  ltsrpr  10487  0nsr  10489  0r  10490  1sr  10491  m1r  10492  addclsr  10493  mulclsr  10494  addcomsr  10497  addasssr  10498  mulcomsr  10499  mulasssr  10500  distrsr  10501  ltsosr  10504  0idsr  10507  1idsr  10508  00sr  10509  ltasr  10510  recexsrlem  10513  mulgt0sr  10515  map2psrpr  10520  wuncn  10580
  Copyright terms: Public domain W3C validator