Definition df-nr 7875

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 7445	. 2 class R.
2		cnp 7439	. . . 4 class P.
3	2, 2	cxp 4691	. . 3 class ( P. X. P. )
4		cer 7444	. . 3 class ~R
5	3, 4	cqs 6642	. 2 class ( ( P. X. P. ) /. ~R )
6	1, 5	wceq 1373	1 wff R. = ( ( P. X. P. ) /. ~R )

This definition is referenced by:  addsrpr  7893  mulsrpr  7894  ltsrprg  7895  gt0srpr  7896  0nsr  7897  0r  7898  1sr  7899  m1r  7900  addclsr  7901  mulclsr  7902  addcomsrg  7903  addasssrg  7904  mulcomsrg  7905  mulasssrg  7906  distrsrg  7907  lttrsr  7910  ltposr  7911  ltsosr  7912  0idsr  7915  1idsr  7916  00sr  7917  ltasrg  7918  recexgt0sr  7921  mulgt0sr  7926  aptisr  7927  mulextsr1  7929  archsr  7930  srpospr  7931  prsrcl  7932  ltpsrprg  7951  mappsrprg  7952  map2psrprg  7953  suplocsrlemb  7954  addvalex  7992  pitonnlem2  7995  pitore  7998  recnnre  7999  axcnex  8007