Definition df-nr 7528

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 7098	. 2 class R
2		cnp 7092	. . . 4 class P
3	2, 2	cxp 4532	. . 3 class (P × P)
4		cer 7097	. . 3 class ~R
5	3, 4	cqs 6421	. 2 class ((P × P) / ~R )
6	1, 5	wceq 1331	1 wff R = ((P × P) / ~R )

This definition is referenced by:  addsrpr  7546  mulsrpr  7547  ltsrprg  7548  gt0srpr  7549  0nsr  7550  0r  7551  1sr  7552  m1r  7553  addclsr  7554  mulclsr  7555  addcomsrg  7556  addasssrg  7557  mulcomsrg  7558  mulasssrg  7559  distrsrg  7560  lttrsr  7563  ltposr  7564  ltsosr  7565  0idsr  7568  1idsr  7569  00sr  7570  ltasrg  7571  recexgt0sr  7574  mulgt0sr  7579  aptisr  7580  mulextsr1  7582  archsr  7583  srpospr  7584  prsrcl  7585  ltpsrprg  7604  mappsrprg  7605  map2psrprg  7606  suplocsrlemb  7607  addvalex  7645  pitonnlem2  7648  pitore  7651  recnnre  7652  axcnex  7660