Definition df-nr 7668

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

Assertion

Ref	Expression
df-nr	⊢ R = ((P × P) / ~R )

Detailed syntax breakdown of Definition df-nr

Step	Hyp	Ref	Expression
1		cnr 7238	. 2 class R
2		cnp 7232	. . . 4 class P
3	2, 2	cxp 4602	. . 3 class (P × P)
4		cer 7237	. . 3 class ~R
5	3, 4	cqs 6500	. 2 class ((P × P) / ~R )
6	1, 5	wceq 1343	1 wff R = ((P × P) / ~R )

This definition is referenced by:  addsrpr  7686  mulsrpr  7687  ltsrprg  7688  gt0srpr  7689  0nsr  7690  0r  7691  1sr  7692  m1r  7693  addclsr  7694  mulclsr  7695  addcomsrg  7696  addasssrg  7697  mulcomsrg  7698  mulasssrg  7699  distrsrg  7700  lttrsr  7703  ltposr  7704  ltsosr  7705  0idsr  7708  1idsr  7709  00sr  7710  ltasrg  7711  recexgt0sr  7714  mulgt0sr  7719  aptisr  7720  mulextsr1  7722  archsr  7723  srpospr  7724  prsrcl  7725  ltpsrprg  7744  mappsrprg  7745  map2psrprg  7746  suplocsrlemb  7747  addvalex  7785  pitonnlem2  7788  pitore  7791  recnnre  7792  axcnex  7800