Definition df-nr 7990

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 7560	. 2 class R
2		cnp 7554	. . . 4 class P
3	2, 2	cxp 4729	. . 3 class (P × P)
4		cer 7559	. . 3 class ~R
5	3, 4	cqs 6744	. 2 class ((P × P) / ~R )
6	1, 5	wceq 1398	1 wff R = ((P × P) / ~R )

This definition is referenced by:  addsrpr  8008  mulsrpr  8009  ltsrprg  8010  gt0srpr  8011  0nsr  8012  0r  8013  1sr  8014  m1r  8015  addclsr  8016  mulclsr  8017  addcomsrg  8018  addasssrg  8019  mulcomsrg  8020  mulasssrg  8021  distrsrg  8022  lttrsr  8025  ltposr  8026  ltsosr  8027  0idsr  8030  1idsr  8031  00sr  8032  ltasrg  8033  recexgt0sr  8036  mulgt0sr  8041  aptisr  8042  mulextsr1  8044  archsr  8045  srpospr  8046  prsrcl  8047  ltpsrprg  8066  mappsrprg  8067  map2psrprg  8068  suplocsrlemb  8069  addvalex  8107  pitonnlem2  8110  pitore  8113  recnnre  8114  axcnex  8122