Definition df-nr 8100

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 × P) / ~R )

Detailed syntax breakdown of Definition df-nr

Step	Hyp	Ref	Expression
1		cnr 7670	. 2 class R
2		cnp 7664	. . . 4 class P
3	2, 2	cxp 4774	. . 3 class (P × P)
4		cer 7669	. . 3 class ~R
5	3, 4	cqs 6810	. 2 class ((P × P) / ~R )
6	1, 5	wceq 1402	1 wff R = ((P × P) / ~R )

This definition is used by:  addsrpr  8118  mulsrpr  8119  ltsrprg  8120  gt0srpr  8121  0nsr  8122  0r  8123  1sr  8124  m1r  8125  addclsr  8126  mulclsr  8127  addcomsrg  8128  addasssrg  8129  mulcomsrg  8130  mulasssrg  8131  distrsrg  8132  lttrsr  8135  ltposr  8136  ltsosr  8137  0idsr  8140  1idsr  8141  00sr  8142  ltasrg  8143  recexgt0sr  8146  mulgt0sr  8151  aptisr  8152  mulextsr1  8154  archsr  8155  srpospr  8156  prsrcl  8157  ltpsrprg  8176  mappsrprg  8177  map2psrprg  8178  suplocsrlemb  8179  addvalex  8217  pitonnlem2  8220  pitore  8223  recnnre  8224  axcnex  8232