Definition df-nr 6812

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 6395	. 2 class R.
2		cnp 6389	. . . 4 class P.
3	2, 2	cxp 4343	. . 3 class ( P. X. P. )
4		cer 6394	. . 3 class ~R
5	3, 4	cqs 6105	. 2 class ( ( P. X. P. ) /. ~R )
6	1, 5	wceq 1243	1 wff R. = ( ( P. X. P. ) /. ~R )

This definition is referenced by:  addsrpr  6830  mulsrpr  6831  ltsrprg  6832  gt0srpr  6833  0nsr  6834  0r  6835  1sr  6836  m1r  6837  addclsr  6838  mulclsr  6839  addcomsrg  6840  addasssrg  6841  mulcomsrg  6842  mulasssrg  6843  distrsrg  6844  lttrsr  6847  ltposr  6848  ltsosr  6849  0idsr  6852  1idsr  6853  00sr  6854  ltasrg  6855  recexgt0sr  6858  mulgt0sr  6862  aptisr  6863  mulextsr1  6865  archsr  6866  srpospr  6867  prsrcl  6868  addvalex  6920  pitonnlem2  6923  pitore  6926  recnnre  6927  axcnex  6935