Definition df-nr 7464

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. X. P. ) /. ~R )

Detailed syntax breakdown of Definition df-nr

Step	Hyp	Ref	Expression
1		cnr 7047	. 2 class R.
2		cnp 7041	. . . 4 class P.
3	2, 2	cxp 4495	. . 3 class ( P. X. P. )
4		cer 7046	. . 3 class ~R
5	3, 4	cqs 6380	. 2 class ( ( P. X. P. ) /. ~R )
6	1, 5	wceq 1312	1 wff R. = ( ( P. X. P. ) /. ~R )

This definition is referenced by:  addsrpr  7482  mulsrpr  7483  ltsrprg  7484  gt0srpr  7485  0nsr  7486  0r  7487  1sr  7488  m1r  7489  addclsr  7490  mulclsr  7491  addcomsrg  7492  addasssrg  7493  mulcomsrg  7494  mulasssrg  7495  distrsrg  7496  lttrsr  7499  ltposr  7500  ltsosr  7501  0idsr  7504  1idsr  7505  00sr  7506  ltasrg  7507  recexgt0sr  7510  mulgt0sr  7514  aptisr  7515  mulextsr1  7517  archsr  7518  srpospr  7519  prsrcl  7520  addvalex  7573  pitonnlem2  7576  pitore  7579  recnnre  7580  axcnex  7588