Definition df-nr 7914

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 7484	. 2 class R.
2		cnp 7478	. . . 4 class P.
3	2, 2	cxp 4717	. . 3 class ( P. X. P. )
4		cer 7483	. . 3 class ~R
5	3, 4	cqs 6679	. 2 class ( ( P. X. P. ) /. ~R )
6	1, 5	wceq 1395	1 wff R. = ( ( P. X. P. ) /. ~R )

This definition is referenced by:  addsrpr  7932  mulsrpr  7933  ltsrprg  7934  gt0srpr  7935  0nsr  7936  0r  7937  1sr  7938  m1r  7939  addclsr  7940  mulclsr  7941  addcomsrg  7942  addasssrg  7943  mulcomsrg  7944  mulasssrg  7945  distrsrg  7946  lttrsr  7949  ltposr  7950  ltsosr  7951  0idsr  7954  1idsr  7955  00sr  7956  ltasrg  7957  recexgt0sr  7960  mulgt0sr  7965  aptisr  7966  mulextsr1  7968  archsr  7969  srpospr  7970  prsrcl  7971  ltpsrprg  7990  mappsrprg  7991  map2psrprg  7992  suplocsrlemb  7993  addvalex  8031  pitonnlem2  8034  pitore  8037  recnnre  8038  axcnex  8046