Definition df-nr 8095

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 7665	. 2 class R.
2		cnp 7659	. . . 4 class P.
3	2, 2	cxp 4772	. . 3 class ( P. X. P. )
4		cer 7664	. . 3 class ~R
5	3, 4	cqs 6806	. 2 class ( ( P. X. P. ) /. ~R )
6	1, 5	wceq 1402	1 wff R. = ( ( P. X. P. ) /. ~R )

This definition is used by:  addsrpr  8113  mulsrpr  8114  ltsrprg  8115  gt0srpr  8116  0nsr  8117  0r  8118  1sr  8119  m1r  8120  addclsr  8121  mulclsr  8122  addcomsrg  8123  addasssrg  8124  mulcomsrg  8125  mulasssrg  8126  distrsrg  8127  lttrsr  8130  ltposr  8131  ltsosr  8132  0idsr  8135  1idsr  8136  00sr  8137  ltasrg  8138  recexgt0sr  8141  mulgt0sr  8146  aptisr  8147  mulextsr1  8149  archsr  8150  srpospr  8151  prsrcl  8152  ltpsrprg  8171  mappsrprg  8172  map2psrprg  8173  suplocsrlemb  8174  addvalex  8212  pitonnlem2  8215  pitore  8218  recnnre  8219  axcnex  8227