Definition df-nr 7946

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 7516	. 2 class R
2		cnp 7510	. . . 4 class P
3	2, 2	cxp 4723	. . 3 class (P × P)
4		cer 7515	. . 3 class ~R
5	3, 4	cqs 6700	. 2 class ((P × P) / ~R )
6	1, 5	wceq 1397	1 wff R = ((P × P) / ~R )

This definition is referenced by:  addsrpr  7964  mulsrpr  7965  ltsrprg  7966  gt0srpr  7967  0nsr  7968  0r  7969  1sr  7970  m1r  7971  addclsr  7972  mulclsr  7973  addcomsrg  7974  addasssrg  7975  mulcomsrg  7976  mulasssrg  7977  distrsrg  7978  lttrsr  7981  ltposr  7982  ltsosr  7983  0idsr  7986  1idsr  7987  00sr  7988  ltasrg  7989  recexgt0sr  7992  mulgt0sr  7997  aptisr  7998  mulextsr1  8000  archsr  8001  srpospr  8002  prsrcl  8003  ltpsrprg  8022  mappsrprg  8023  map2psrprg  8024  suplocsrlemb  8025  addvalex  8063  pitonnlem2  8066  pitore  8069  recnnre  8070  axcnex  8078