Definition df-nr 7535

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 7105	. 2 class R.
2		cnp 7099	. . . 4 class P.
3	2, 2	cxp 4537	. . 3 class ( P. X. P. )
4		cer 7104	. . 3 class ~R
5	3, 4	cqs 6428	. 2 class ( ( P. X. P. ) /. ~R )
6	1, 5	wceq 1331	1 wff R. = ( ( P. X. P. ) /. ~R )

This definition is referenced by:  addsrpr  7553  mulsrpr  7554  ltsrprg  7555  gt0srpr  7556  0nsr  7557  0r  7558  1sr  7559  m1r  7560  addclsr  7561  mulclsr  7562  addcomsrg  7563  addasssrg  7564  mulcomsrg  7565  mulasssrg  7566  distrsrg  7567  lttrsr  7570  ltposr  7571  ltsosr  7572  0idsr  7575  1idsr  7576  00sr  7577  ltasrg  7578  recexgt0sr  7581  mulgt0sr  7586  aptisr  7587  mulextsr1  7589  archsr  7590  srpospr  7591  prsrcl  7592  ltpsrprg  7611  mappsrprg  7612  map2psrprg  7613  suplocsrlemb  7614  addvalex  7652  pitonnlem2  7655  pitore  7658  recnnre  7659  axcnex  7667