MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-nr Unicode version

Definition df-nr 9455
Description: Define class of signed reals. This is a "temporary" set used in the construction of complex numbers df-c 9519, 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

Detailed syntax breakdown of Definition df-nr
StepHypRef Expression
1 cnr 9264 . 2
2 cnp 9258 . . . 4
32, 2cxp 5002 . . 3
4 cer 9263 . . 3
53, 4cqs 7329 . 2
61, 5wceq 1395 1
Colors of variables: wff setvar class
This definition is referenced by:  addsrpr  9473  mulsrpr  9474  ltsrpr  9475  0nsr  9477  0r  9478  1sr  9479  m1r  9480  addclsr  9481  mulclsr  9482  addcomsr  9485  addasssr  9486  mulcomsr  9487  mulasssr  9488  distrsr  9489  ltsosr  9492  0idsr  9495  1idsr  9496  00sr  9497  ltasr  9498  recexsrlem  9501  mulgt0sr  9503  map2psrpr  9508  axcnex  9545  wuncn  9568
  Copyright terms: Public domain W3C validator