Definition df-nr 7689

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 7259	. 2 class R
2		cnp 7253	. . . 4 class P
3	2, 2	cxp 4609	. . 3 class (P × P)
4		cer 7258	. . 3 class ~R
5	3, 4	cqs 6512	. 2 class ((P × P) / ~R )
6	1, 5	wceq 1348	1 wff R = ((P × P) / ~R )

This definition is referenced by:  addsrpr  7707  mulsrpr  7708  ltsrprg  7709  gt0srpr  7710  0nsr  7711  0r  7712  1sr  7713  m1r  7714  addclsr  7715  mulclsr  7716  addcomsrg  7717  addasssrg  7718  mulcomsrg  7719  mulasssrg  7720  distrsrg  7721  lttrsr  7724  ltposr  7725  ltsosr  7726  0idsr  7729  1idsr  7730  00sr  7731  ltasrg  7732  recexgt0sr  7735  mulgt0sr  7740  aptisr  7741  mulextsr1  7743  archsr  7744  srpospr  7745  prsrcl  7746  ltpsrprg  7765  mappsrprg  7766  map2psrprg  7767  suplocsrlemb  7768  addvalex  7806  pitonnlem2  7809  pitore  7812  recnnre  7813  axcnex  7821