Definition df-nr 7559

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 7129	. 2 class R
2		cnp 7123	. . . 4 class P
3	2, 2	cxp 4545	. . 3 class (P × P)
4		cer 7128	. . 3 class ~R
5	3, 4	cqs 6436	. 2 class ((P × P) / ~R )
6	1, 5	wceq 1332	1 wff R = ((P × P) / ~R )

This definition is referenced by:  addsrpr  7577  mulsrpr  7578  ltsrprg  7579  gt0srpr  7580  0nsr  7581  0r  7582  1sr  7583  m1r  7584  addclsr  7585  mulclsr  7586  addcomsrg  7587  addasssrg  7588  mulcomsrg  7589  mulasssrg  7590  distrsrg  7591  lttrsr  7594  ltposr  7595  ltsosr  7596  0idsr  7599  1idsr  7600  00sr  7601  ltasrg  7602  recexgt0sr  7605  mulgt0sr  7610  aptisr  7611  mulextsr1  7613  archsr  7614  srpospr  7615  prsrcl  7616  ltpsrprg  7635  mappsrprg  7636  map2psrprg  7637  suplocsrlemb  7638  addvalex  7676  pitonnlem2  7679  pitore  7682  recnnre  7683  axcnex  7691