Definition df-nr 8042

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 7612	. 2 class R.
2		cnp 7606	. . . 4 class P.
3	2, 2	cxp 4747	. . 3 class ( P. X. P. )
4		cer 7611	. . 3 class ~R
5	3, 4	cqs 6766	. 2 class ( ( P. X. P. ) /. ~R )
6	1, 5	wceq 1398	1 wff R. = ( ( P. X. P. ) /. ~R )

This definition is referenced by:  addsrpr  8060  mulsrpr  8061  ltsrprg  8062  gt0srpr  8063  0nsr  8064  0r  8065  1sr  8066  m1r  8067  addclsr  8068  mulclsr  8069  addcomsrg  8070  addasssrg  8071  mulcomsrg  8072  mulasssrg  8073  distrsrg  8074  lttrsr  8077  ltposr  8078  ltsosr  8079  0idsr  8082  1idsr  8083  00sr  8084  ltasrg  8085  recexgt0sr  8088  mulgt0sr  8093  aptisr  8094  mulextsr1  8096  archsr  8097  srpospr  8098  prsrcl  8099  ltpsrprg  8118  mappsrprg  8119  map2psrprg  8120  suplocsrlemb  8121  addvalex  8159  pitonnlem2  8162  pitore  8165  recnnre  8166  axcnex  8174