Definition df-nr 8094

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

This definition is used by:  addsrpr  8112  mulsrpr  8113  ltsrprg  8114  gt0srpr  8115  0nsr  8116  0r  8117  1sr  8118  m1r  8119  addclsr  8120  mulclsr  8121  addcomsrg  8122  addasssrg  8123  mulcomsrg  8124  mulasssrg  8125  distrsrg  8126  lttrsr  8129  ltposr  8130  ltsosr  8131  0idsr  8134  1idsr  8135  00sr  8136  ltasrg  8137  recexgt0sr  8140  mulgt0sr  8145  aptisr  8146  mulextsr1  8148  archsr  8149  srpospr  8150  prsrcl  8151  ltpsrprg  8170  mappsrprg  8171  map2psrprg  8172  suplocsrlemb  8173  addvalex  8211  pitonnlem2  8214  pitore  8217  recnnre  8218  axcnex  8226