Definition df-nr 7860

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 7430	. 2 class R
2		cnp 7424	. . . 4 class P
3	2, 2	cxp 4681	. . 3 class (P × P)
4		cer 7429	. . 3 class ~R
5	3, 4	cqs 6632	. 2 class ((P × P) / ~R )
6	1, 5	wceq 1373	1 wff R = ((P × P) / ~R )

This definition is referenced by:  addsrpr  7878  mulsrpr  7879  ltsrprg  7880  gt0srpr  7881  0nsr  7882  0r  7883  1sr  7884  m1r  7885  addclsr  7886  mulclsr  7887  addcomsrg  7888  addasssrg  7889  mulcomsrg  7890  mulasssrg  7891  distrsrg  7892  lttrsr  7895  ltposr  7896  ltsosr  7897  0idsr  7900  1idsr  7901  00sr  7902  ltasrg  7903  recexgt0sr  7906  mulgt0sr  7911  aptisr  7912  mulextsr1  7914  archsr  7915  srpospr  7916  prsrcl  7917  ltpsrprg  7936  mappsrprg  7937  map2psrprg  7938  suplocsrlemb  7939  addvalex  7977  pitonnlem2  7980  pitore  7983  recnnre  7984  axcnex  7992