Definition df-nr 6904

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 6487	. 2 class R.
2		cnp 6481	. . . 4 class P.
3	2, 2	cxp 4361	. . 3 class ( P. X. P. )
4		cer 6486	. . 3 class ~R
5	3, 4	cqs 6128	. 2 class ( ( P. X. P. ) /. ~R )
6	1, 5	wceq 1284	1 wff R. = ( ( P. X. P. ) /. ~R )

This definition is referenced by:  addsrpr  6922  mulsrpr  6923  ltsrprg  6924  gt0srpr  6925  0nsr  6926  0r  6927  1sr  6928  m1r  6929  addclsr  6930  mulclsr  6931  addcomsrg  6932  addasssrg  6933  mulcomsrg  6934  mulasssrg  6935  distrsrg  6936  lttrsr  6939  ltposr  6940  ltsosr  6941  0idsr  6944  1idsr  6945  00sr  6946  ltasrg  6947  recexgt0sr  6950  mulgt0sr  6954  aptisr  6955  mulextsr1  6957  archsr  6958  srpospr  6959  prsrcl  6960  addvalex  7012  pitonnlem2  7015  pitore  7018  recnnre  7019  axcnex  7027