Definition df-nr 7813

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 7383	. 2 class R
2		cnp 7377	. . . 4 class P
3	2, 2	cxp 4662	. . 3 class (P × P)
4		cer 7382	. . 3 class ~R
5	3, 4	cqs 6600	. 2 class ((P × P) / ~R )
6	1, 5	wceq 1364	1 wff R = ((P × P) / ~R )

This definition is referenced by:  addsrpr  7831  mulsrpr  7832  ltsrprg  7833  gt0srpr  7834  0nsr  7835  0r  7836  1sr  7837  m1r  7838  addclsr  7839  mulclsr  7840  addcomsrg  7841  addasssrg  7842  mulcomsrg  7843  mulasssrg  7844  distrsrg  7845  lttrsr  7848  ltposr  7849  ltsosr  7850  0idsr  7853  1idsr  7854  00sr  7855  ltasrg  7856  recexgt0sr  7859  mulgt0sr  7864  aptisr  7865  mulextsr1  7867  archsr  7868  srpospr  7869  prsrcl  7870  ltpsrprg  7889  mappsrprg  7890  map2psrprg  7891  suplocsrlemb  7892  addvalex  7930  pitonnlem2  7933  pitore  7936  recnnre  7937  axcnex  7945