Definition df-nr 6655

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. X. P.) /. ~R )

Detailed syntax breakdown of Definition df-nr

Step	Hyp	Ref	Expression
1		cnr 6281	. 2 class R.
2		cnp 6275	. . . 4 class P.
3	2, 2	cxp 4286	. . 3 class ( P. X. P.)
4		cer 6280	. . 3 class ~R
5	3, 4	cqs 6041	. 2 class (( P. X. P.) /. ~R )
6	1, 5	wceq 1242	1 wff R. = (( P. X. P.) /. ~R )

This definition is referenced by:  addsrpr  6673  mulsrpr  6674  ltsrprg  6675  gt0srpr  6676  0nsr  6677  0r  6678  1sr  6679  m1r  6680  addclsr  6681  mulclsr  6682  addcomsrg  6683  addasssrg  6684  mulcomsrg  6685  mulasssrg  6686  distrsrg  6687  lttrsr  6690  ltposr  6691  ltsosr  6692  0idsr  6695  1idsr  6696  00sr  6697  ltasrg  6698  recexgt0sr  6701  mulgt0sr  6704  aptisr  6705  mulextsr1  6707  archsr  6708  pitonnlem2  6743  axcnex  6745