Definition df-nr 7789

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 7359	. 2 class R
2		cnp 7353	. . . 4 class P
3	2, 2	cxp 4658	. . 3 class (P × P)
4		cer 7358	. . 3 class ~R
5	3, 4	cqs 6588	. 2 class ((P × P) / ~R )
6	1, 5	wceq 1364	1 wff R = ((P × P) / ~R )

This definition is referenced by:  addsrpr  7807  mulsrpr  7808  ltsrprg  7809  gt0srpr  7810  0nsr  7811  0r  7812  1sr  7813  m1r  7814  addclsr  7815  mulclsr  7816  addcomsrg  7817  addasssrg  7818  mulcomsrg  7819  mulasssrg  7820  distrsrg  7821  lttrsr  7824  ltposr  7825  ltsosr  7826  0idsr  7829  1idsr  7830  00sr  7831  ltasrg  7832  recexgt0sr  7835  mulgt0sr  7840  aptisr  7841  mulextsr1  7843  archsr  7844  srpospr  7845  prsrcl  7846  ltpsrprg  7865  mappsrprg  7866  map2psrprg  7867  suplocsrlemb  7868  addvalex  7906  pitonnlem2  7909  pitore  7912  recnnre  7913  axcnex  7921