Definition df-nr 7647

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 7217	. 2 class R
2		cnp 7211	. . . 4 class P
3	2, 2	cxp 4584	. . 3 class (P × P)
4		cer 7216	. . 3 class ~R
5	3, 4	cqs 6479	. 2 class ((P × P) / ~R )
6	1, 5	wceq 1335	1 wff R = ((P × P) / ~R )

This definition is referenced by:  addsrpr  7665  mulsrpr  7666  ltsrprg  7667  gt0srpr  7668  0nsr  7669  0r  7670  1sr  7671  m1r  7672  addclsr  7673  mulclsr  7674  addcomsrg  7675  addasssrg  7676  mulcomsrg  7677  mulasssrg  7678  distrsrg  7679  lttrsr  7682  ltposr  7683  ltsosr  7684  0idsr  7687  1idsr  7688  00sr  7689  ltasrg  7690  recexgt0sr  7693  mulgt0sr  7698  aptisr  7699  mulextsr1  7701  archsr  7702  srpospr  7703  prsrcl  7704  ltpsrprg  7723  mappsrprg  7724  map2psrprg  7725  suplocsrlemb  7726  addvalex  7764  pitonnlem2  7767  pitore  7770  recnnre  7771  axcnex  7779