Definition df-nr 7842

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 7412	. 2 class R.
2		cnp 7406	. . . 4 class P.
3	2, 2	cxp 4674	. . 3 class ( P. X. P. )
4		cer 7411	. . 3 class ~R
5	3, 4	cqs 6621	. 2 class ( ( P. X. P. ) /. ~R )
6	1, 5	wceq 1373	1 wff R. = ( ( P. X. P. ) /. ~R )

This definition is referenced by:  addsrpr  7860  mulsrpr  7861  ltsrprg  7862  gt0srpr  7863  0nsr  7864  0r  7865  1sr  7866  m1r  7867  addclsr  7868  mulclsr  7869  addcomsrg  7870  addasssrg  7871  mulcomsrg  7872  mulasssrg  7873  distrsrg  7874  lttrsr  7877  ltposr  7878  ltsosr  7879  0idsr  7882  1idsr  7883  00sr  7884  ltasrg  7885  recexgt0sr  7888  mulgt0sr  7893  aptisr  7894  mulextsr1  7896  archsr  7897  srpospr  7898  prsrcl  7899  ltpsrprg  7918  mappsrprg  7919  map2psrprg  7920  suplocsrlemb  7921  addvalex  7959  pitonnlem2  7962  pitore  7965  recnnre  7966  axcnex  7974