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 9991
Description: Define class of signed reals. This is a "temporary" set used in the construction of complex numbers df-c 10055, 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 9800 . 2 class R
2 cnp 9794 . . . 4 class P
32, 2cxp 5216 . . 3 class (P × P)
4 cer 9799 . . 3 class ~R
53, 4cqs 7861 . 2 class ((P × P) / ~R )
61, 5wceq 1596 1 wff R = ((P × P) / ~R )
Colors of variables: wff setvar class
This definition is referenced by:  addsrpr  10009  mulsrpr  10010  ltsrpr  10011  0nsr  10013  0r  10014  1sr  10015  m1r  10016  addclsr  10017  mulclsr  10018  addcomsr  10021  addasssr  10022  mulcomsr  10023  mulasssr  10024  distrsr  10025  ltsosr  10028  0idsr  10031  1idsr  10032  00sr  10033  ltasr  10034  recexsrlem  10037  mulgt0sr  10039  map2psrpr  10044  axcnex  10081  wuncn  10104
  Copyright terms: Public domain W3C validator