Definition df-nr 7811

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 7381	. 2 class R.
2		cnp 7375	. . . 4 class P.
3	2, 2	cxp 4662	. . 3 class ( P. X. P. )
4		cer 7380	. . 3 class ~R
5	3, 4	cqs 6600	. 2 class ( ( P. X. P. ) /. ~R )
6	1, 5	wceq 1364	1 wff R. = ( ( P. X. P. ) /. ~R )

This definition is referenced by:  addsrpr  7829  mulsrpr  7830  ltsrprg  7831  gt0srpr  7832  0nsr  7833  0r  7834  1sr  7835  m1r  7836  addclsr  7837  mulclsr  7838  addcomsrg  7839  addasssrg  7840  mulcomsrg  7841  mulasssrg  7842  distrsrg  7843  lttrsr  7846  ltposr  7847  ltsosr  7848  0idsr  7851  1idsr  7852  00sr  7853  ltasrg  7854  recexgt0sr  7857  mulgt0sr  7862  aptisr  7863  mulextsr1  7865  archsr  7866  srpospr  7867  prsrcl  7868  ltpsrprg  7887  mappsrprg  7888  map2psrprg  7889  suplocsrlemb  7890  addvalex  7928  pitonnlem2  7931  pitore  7934  recnnre  7935  axcnex  7943