Definition df-nr 7728

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 7298	. 2 class R.
2		cnp 7292	. . . 4 class P.
3	2, 2	cxp 4626	. . 3 class ( P. X. P. )
4		cer 7297	. . 3 class ~R
5	3, 4	cqs 6536	. 2 class ( ( P. X. P. ) /. ~R )
6	1, 5	wceq 1353	1 wff R. = ( ( P. X. P. ) /. ~R )

This definition is referenced by:  addsrpr  7746  mulsrpr  7747  ltsrprg  7748  gt0srpr  7749  0nsr  7750  0r  7751  1sr  7752  m1r  7753  addclsr  7754  mulclsr  7755  addcomsrg  7756  addasssrg  7757  mulcomsrg  7758  mulasssrg  7759  distrsrg  7760  lttrsr  7763  ltposr  7764  ltsosr  7765  0idsr  7768  1idsr  7769  00sr  7770  ltasrg  7771  recexgt0sr  7774  mulgt0sr  7779  aptisr  7780  mulextsr1  7782  archsr  7783  srpospr  7784  prsrcl  7785  ltpsrprg  7804  mappsrprg  7805  map2psrprg  7806  suplocsrlemb  7807  addvalex  7845  pitonnlem2  7848  pitore  7851  recnnre  7852  axcnex  7860