Definition df-nr 7787

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 7357	. 2 class R
2		cnp 7351	. . . 4 class P
3	2, 2	cxp 4657	. . 3 class (P × P)
4		cer 7356	. . 3 class ~R
5	3, 4	cqs 6586	. 2 class ((P × P) / ~R )
6	1, 5	wceq 1364	1 wff R = ((P × P) / ~R )

This definition is referenced by:  addsrpr  7805  mulsrpr  7806  ltsrprg  7807  gt0srpr  7808  0nsr  7809  0r  7810  1sr  7811  m1r  7812  addclsr  7813  mulclsr  7814  addcomsrg  7815  addasssrg  7816  mulcomsrg  7817  mulasssrg  7818  distrsrg  7819  lttrsr  7822  ltposr  7823  ltsosr  7824  0idsr  7827  1idsr  7828  00sr  7829  ltasrg  7830  recexgt0sr  7833  mulgt0sr  7838  aptisr  7839  mulextsr1  7841  archsr  7842  srpospr  7843  prsrcl  7844  ltpsrprg  7863  mappsrprg  7864  map2psrprg  7865  suplocsrlemb  7866  addvalex  7904  pitonnlem2  7907  pitore  7910  recnnre  7911  axcnex  7919