Definition df-nr 7935

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 7505	. 2 class R.
2		cnp 7499	. . . 4 class P.
3	2, 2	cxp 4719	. . 3 class ( P. X. P. )
4		cer 7504	. . 3 class ~R
5	3, 4	cqs 6694	. 2 class ( ( P. X. P. ) /. ~R )
6	1, 5	wceq 1395	1 wff R. = ( ( P. X. P. ) /. ~R )

This definition is referenced by:  addsrpr  7953  mulsrpr  7954  ltsrprg  7955  gt0srpr  7956  0nsr  7957  0r  7958  1sr  7959  m1r  7960  addclsr  7961  mulclsr  7962  addcomsrg  7963  addasssrg  7964  mulcomsrg  7965  mulasssrg  7966  distrsrg  7967  lttrsr  7970  ltposr  7971  ltsosr  7972  0idsr  7975  1idsr  7976  00sr  7977  ltasrg  7978  recexgt0sr  7981  mulgt0sr  7986  aptisr  7987  mulextsr1  7989  archsr  7990  srpospr  7991  prsrcl  7992  ltpsrprg  8011  mappsrprg  8012  map2psrprg  8013  suplocsrlemb  8014  addvalex  8052  pitonnlem2  8055  pitore  8058  recnnre  8059  axcnex  8067