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 9838
Description: Define class of signed reals. This is a "temporary" set used in the construction of complex numbers df-c 9902, 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 9647 . 2 class R
2 cnp 9641 . . . 4 class P
32, 2cxp 5082 . . 3 class (P × P)
4 cer 9646 . . 3 class ~R
53, 4cqs 7701 . 2 class ((P × P) / ~R )
61, 5wceq 1480 1 wff R = ((P × P) / ~R )
Colors of variables: wff setvar class
This definition is referenced by:  addsrpr  9856  mulsrpr  9857  ltsrpr  9858  0nsr  9860  0r  9861  1sr  9862  m1r  9863  addclsr  9864  mulclsr  9865  addcomsr  9868  addasssr  9869  mulcomsr  9870  mulasssr  9871  distrsr  9872  ltsosr  9875  0idsr  9878  1idsr  9879  00sr  9880  ltasr  9881  recexsrlem  9884  mulgt0sr  9886  map2psrpr  9891  axcnex  9928  wuncn  9951
  Copyright terms: Public domain W3C validator