Definition df-nr 8058

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 7628	. 2 class R.
2		cnp 7622	. . . 4 class P.
3	2, 2	cxp 4752	. . 3 class ( P. X. P. )
4		cer 7627	. . 3 class ~R
5	3, 4	cqs 6779	. 2 class ( ( P. X. P. ) /. ~R )
6	1, 5	wceq 1398	1 wff R. = ( ( P. X. P. ) /. ~R )

This definition is referenced by:  addsrpr  8076  mulsrpr  8077  ltsrprg  8078  gt0srpr  8079  0nsr  8080  0r  8081  1sr  8082  m1r  8083  addclsr  8084  mulclsr  8085  addcomsrg  8086  addasssrg  8087  mulcomsrg  8088  mulasssrg  8089  distrsrg  8090  lttrsr  8093  ltposr  8094  ltsosr  8095  0idsr  8098  1idsr  8099  00sr  8100  ltasrg  8101  recexgt0sr  8104  mulgt0sr  8109  aptisr  8110  mulextsr1  8112  archsr  8113  srpospr  8114  prsrcl  8115  ltpsrprg  8134  mappsrprg  8135  map2psrprg  8136  suplocsrlemb  8137  addvalex  8175  pitonnlem2  8178  pitore  8181  recnnre  8182  axcnex  8190