Definition df-nr 7822

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 7392	. 2 class R
2		cnp 7386	. . . 4 class P
3	2, 2	cxp 4671	. . 3 class (P × P)
4		cer 7391	. . 3 class ~R
5	3, 4	cqs 6609	. 2 class ((P × P) / ~R )
6	1, 5	wceq 1372	1 wff R = ((P × P) / ~R )

This definition is referenced by:  addsrpr  7840  mulsrpr  7841  ltsrprg  7842  gt0srpr  7843  0nsr  7844  0r  7845  1sr  7846  m1r  7847  addclsr  7848  mulclsr  7849  addcomsrg  7850  addasssrg  7851  mulcomsrg  7852  mulasssrg  7853  distrsrg  7854  lttrsr  7857  ltposr  7858  ltsosr  7859  0idsr  7862  1idsr  7863  00sr  7864  ltasrg  7865  recexgt0sr  7868  mulgt0sr  7873  aptisr  7874  mulextsr1  7876  archsr  7877  srpospr  7878  prsrcl  7879  ltpsrprg  7898  mappsrprg  7899  map2psrprg  7900  suplocsrlemb  7901  addvalex  7939  pitonnlem2  7942  pitore  7945  recnnre  7946  axcnex  7954