Definition df-nr 6762

Description: Define class of signed reals. This is a "temporary" set used in the construction of complex numbers df-c 6835, and is intended to be used only by the construction. From Proposition 9-4.2 of [Gleason] p. 126.

Assertion

Ref	Expression
df-nr	|- R. = ((P. X. P.)/. ~R )

Detailed syntax breakdown of Definition df-nr

Step	Hyp	Ref	Expression
1		cnr 6588	. 2 class R.
2		cnp 6580	. . . 4 class P.
3	2, 2	cxp 4149	. . 3 class (P. X. P.)
4		cer 6587	. . 3 class ~R
5	3, 4	cqs 5518	. 2 class ((P. X. P.)/. ~R )
6	1, 5	wceq 1615	1 wff R. = ((P. X. P.)/. ~R )

This definition is referenced by:  srex 6774  addsrpr 6779  mulsrpr 6780  ltsrpr 6781  0nsr 6783  0r 6784  1sr 6785  m1r 6786  addclsr 6787  mulclsr 6788  addcomsr 6791  addasssr 6792  mulcomsr 6793  mulasssr 6794  distrsr 6795  ltsosr 6798  0idsr 6801  1idsr 6802  00sr 6803  ltasr 6804  recexsrlem 6807  mulgt0sr 6809  map2psrpr 6815

Copyright terms: Public domain