Definition df-nr 8007

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 7577	. 2 class R.
2		cnp 7571	. . . 4 class P.
3	2, 2	cxp 4729	. . 3 class ( P. X. P. )
4		cer 7576	. . 3 class ~R
5	3, 4	cqs 6744	. 2 class ( ( P. X. P. ) /. ~R )
6	1, 5	wceq 1398	1 wff R. = ( ( P. X. P. ) /. ~R )

This definition is referenced by:  addsrpr  8025  mulsrpr  8026  ltsrprg  8027  gt0srpr  8028  0nsr  8029  0r  8030  1sr  8031  m1r  8032  addclsr  8033  mulclsr  8034  addcomsrg  8035  addasssrg  8036  mulcomsrg  8037  mulasssrg  8038  distrsrg  8039  lttrsr  8042  ltposr  8043  ltsosr  8044  0idsr  8047  1idsr  8048  00sr  8049  ltasrg  8050  recexgt0sr  8053  mulgt0sr  8058  aptisr  8059  mulextsr1  8061  archsr  8062  srpospr  8063  prsrcl  8064  ltpsrprg  8083  mappsrprg  8084  map2psrprg  8085  suplocsrlemb  8086  addvalex  8124  pitonnlem2  8127  pitore  8130  recnnre  8131  axcnex  8139