Definition df-nr 5139

Description: Define class of signed reals. This is a "temporary" set used in the construction of complex numbers df-c 5212, 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 4965	. 2 class R.
2		cnp 4957	. . . 4 class P.
3	2, 2	cxp 3158	. . 3 class (P. X. P.)
4		cer 4964	. . 3 class ~R
5	3, 4	cqs 4244	. 2 class ((P. X. P.)/. ~R )
6	1, 5	wceq 953	1 wff R. = ((P. X. P.)/. ~R )

This definition is referenced by:  srex 5151  addsrpr 5156  mulsrpr 5157  ltsrpr 5158  0nsr 5160  0r 5161  1r 5162  m1r 5163  addclsr 5164  mulclsr 5165  addcomsr 5168  addasssr 5169  mulcomsr 5170  mulasssr 5171  distrsr 5172  ltsosr 5175  0idsr 5178  1idsr 5179  00sr 5180  ltasr 5181  recexsrlem 5184  mulgt0sr 5186  map2psrpr 5192

Copyright terms: Public domain