Definition df-nr 7840

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 7410	. 2 class R.
2		cnp 7404	. . . 4 class P.
3	2, 2	cxp 4673	. . 3 class ( P. X. P. )
4		cer 7409	. . 3 class ~R
5	3, 4	cqs 6619	. 2 class ( ( P. X. P. ) /. ~R )
6	1, 5	wceq 1373	1 wff R. = ( ( P. X. P. ) /. ~R )

This definition is referenced by:  addsrpr  7858  mulsrpr  7859  ltsrprg  7860  gt0srpr  7861  0nsr  7862  0r  7863  1sr  7864  m1r  7865  addclsr  7866  mulclsr  7867  addcomsrg  7868  addasssrg  7869  mulcomsrg  7870  mulasssrg  7871  distrsrg  7872  lttrsr  7875  ltposr  7876  ltsosr  7877  0idsr  7880  1idsr  7881  00sr  7882  ltasrg  7883  recexgt0sr  7886  mulgt0sr  7891  aptisr  7892  mulextsr1  7894  archsr  7895  srpospr  7896  prsrcl  7897  ltpsrprg  7916  mappsrprg  7917  map2psrprg  7918  suplocsrlemb  7919  addvalex  7957  pitonnlem2  7960  pitore  7963  recnnre  7964  axcnex  7972