Definition df-nr 7839

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 7409	. 2 class R
2		cnp 7403	. . . 4 class P
3	2, 2	cxp 4672	. . 3 class (P × P)
4		cer 7408	. . 3 class ~R
5	3, 4	cqs 6618	. 2 class ((P × P) / ~R )
6	1, 5	wceq 1372	1 wff R = ((P × P) / ~R )

This definition is referenced by:  addsrpr  7857  mulsrpr  7858  ltsrprg  7859  gt0srpr  7860  0nsr  7861  0r  7862  1sr  7863  m1r  7864  addclsr  7865  mulclsr  7866  addcomsrg  7867  addasssrg  7868  mulcomsrg  7869  mulasssrg  7870  distrsrg  7871  lttrsr  7874  ltposr  7875  ltsosr  7876  0idsr  7879  1idsr  7880  00sr  7881  ltasrg  7882  recexgt0sr  7885  mulgt0sr  7890  aptisr  7891  mulextsr1  7893  archsr  7894  srpospr  7895  prsrcl  7896  ltpsrprg  7915  mappsrprg  7916  map2psrprg  7917  suplocsrlemb  7918  addvalex  7956  pitonnlem2  7959  pitore  7962  recnnre  7963  axcnex  7971