Definition df-nr 5167

Description: Define class of signed reals. This is a "temporary" set used in the construction of complex numbers df-c 5240, 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 4993	. 2 class R.
2		cnp 4985	. . . 4 class P.
3	2, 2	cxp 3168	. . 3 class (P. X. P.)
4		cer 4992	. . 3 class ~R
5	3, 4	cqs 4260	. 2 class ((P. X. P.)/. ~R )
6	1, 5	wceq 956	1 wff R. = ((P. X. P.)/. ~R )

This definition is referenced by:  srex 5179  addsrpr 5184  mulsrpr 5185  ltsrpr 5186  0nsr 5188  0r 5189  1r 5190  m1r 5191  addclsr 5192  mulclsr 5193  addcomsr 5196  addasssr 5197  mulcomsr 5198  mulasssr 5199  distrsr 5200  ltsosr 5203  0idsr 5206  1idsr 5207  00sr 5208  ltasr 5209  recexsrlem 5212  mulgt0sr 5214  map2psrpr 5220

Copyright terms: Public domain