Definition df-nr 7947

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

This definition is referenced by:  addsrpr  7965  mulsrpr  7966  ltsrprg  7967  gt0srpr  7968  0nsr  7969  0r  7970  1sr  7971  m1r  7972  addclsr  7973  mulclsr  7974  addcomsrg  7975  addasssrg  7976  mulcomsrg  7977  mulasssrg  7978  distrsrg  7979  lttrsr  7982  ltposr  7983  ltsosr  7984  0idsr  7987  1idsr  7988  00sr  7989  ltasrg  7990  recexgt0sr  7993  mulgt0sr  7998  aptisr  7999  mulextsr1  8001  archsr  8002  srpospr  8003  prsrcl  8004  ltpsrprg  8023  mappsrprg  8024  map2psrprg  8025  suplocsrlemb  8026  addvalex  8064  pitonnlem2  8067  pitore  8070  recnnre  8071  axcnex  8079