Definition df-nr 7725

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 7295	. 2 class R
2		cnp 7289	. . . 4 class P
3	2, 2	cxp 4624	. . 3 class (P × P)
4		cer 7294	. . 3 class ~R
5	3, 4	cqs 6533	. 2 class ((P × P) / ~R )
6	1, 5	wceq 1353	1 wff R = ((P × P) / ~R )

This definition is referenced by:  addsrpr  7743  mulsrpr  7744  ltsrprg  7745  gt0srpr  7746  0nsr  7747  0r  7748  1sr  7749  m1r  7750  addclsr  7751  mulclsr  7752  addcomsrg  7753  addasssrg  7754  mulcomsrg  7755  mulasssrg  7756  distrsrg  7757  lttrsr  7760  ltposr  7761  ltsosr  7762  0idsr  7765  1idsr  7766  00sr  7767  ltasrg  7768  recexgt0sr  7771  mulgt0sr  7776  aptisr  7777  mulextsr1  7779  archsr  7780  srpospr  7781  prsrcl  7782  ltpsrprg  7801  mappsrprg  7802  map2psrprg  7803  suplocsrlemb  7804  addvalex  7842  pitonnlem2  7845  pitore  7848  recnnre  7849  axcnex  7857