Definition df-nr 5179

Description: Define class of signed reals. This is a "temporary" set used in the construction of complex numbers df-c 5252, 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 5005	. 2 class R.
2		cnp 4997	. . . 4 class P.
3	2, 2	cxp 3174	. . 3 class (P. X. P.)
4		cer 5004	. . 3 class ~R
5	3, 4	cqs 4266	. 2 class ((P. X. P.)/. ~R )
6	1, 5	wceq 958	1 wff R. = ((P. X. P.)/. ~R )

This definition is referenced by:  srex 5191  addsrpr 5196  mulsrpr 5197  ltsrpr 5198  0nsr 5200  0r 5201  1r 5202  m1r 5203  addclsr 5204  mulclsr 5205  addcomsr 5208  addasssr 5209  mulcomsr 5210  mulasssr 5211  distrsr 5212  ltsosr 5215  0idsr 5218  1idsr 5219  00sr 5220  ltasr 5221  recexsrlem 5224  mulgt0sr 5226  map2psrpr 5232

Copyright terms: Public domain