Definition df-nr 7925

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 7495	. 2 class R
2		cnp 7489	. . . 4 class P
3	2, 2	cxp 4717	. . 3 class (P × P)
4		cer 7494	. . 3 class ~R
5	3, 4	cqs 6687	. 2 class ((P × P) / ~R )
6	1, 5	wceq 1395	1 wff R = ((P × P) / ~R )

This definition is referenced by:  addsrpr  7943  mulsrpr  7944  ltsrprg  7945  gt0srpr  7946  0nsr  7947  0r  7948  1sr  7949  m1r  7950  addclsr  7951  mulclsr  7952  addcomsrg  7953  addasssrg  7954  mulcomsrg  7955  mulasssrg  7956  distrsrg  7957  lttrsr  7960  ltposr  7961  ltsosr  7962  0idsr  7965  1idsr  7966  00sr  7967  ltasrg  7968  recexgt0sr  7971  mulgt0sr  7976  aptisr  7977  mulextsr1  7979  archsr  7980  srpospr  7981  prsrcl  7982  ltpsrprg  8001  mappsrprg  8002  map2psrprg  8003  suplocsrlemb  8004  addvalex  8042  pitonnlem2  8045  pitore  8048  recnnre  8049  axcnex  8057