Definition df-nr 7726

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 7296	. 2 class R
2		cnp 7290	. . . 4 class P
3	2, 2	cxp 4625	. . 3 class (P × P)
4		cer 7295	. . 3 class ~R
5	3, 4	cqs 6534	. 2 class ((P × P) / ~R )
6	1, 5	wceq 1353	1 wff R = ((P × P) / ~R )

This definition is referenced by:  addsrpr  7744  mulsrpr  7745  ltsrprg  7746  gt0srpr  7747  0nsr  7748  0r  7749  1sr  7750  m1r  7751  addclsr  7752  mulclsr  7753  addcomsrg  7754  addasssrg  7755  mulcomsrg  7756  mulasssrg  7757  distrsrg  7758  lttrsr  7761  ltposr  7762  ltsosr  7763  0idsr  7766  1idsr  7767  00sr  7768  ltasrg  7769  recexgt0sr  7772  mulgt0sr  7777  aptisr  7778  mulextsr1  7780  archsr  7781  srpospr  7782  prsrcl  7783  ltpsrprg  7802  mappsrprg  7803  map2psrprg  7804  suplocsrlemb  7805  addvalex  7843  pitonnlem2  7846  pitore  7849  recnnre  7850  axcnex  7858