Definition df-nr 5321

Description: Define class of signed reals. This is a "temporary" set used in the construction of complex numbers df-c 5394, 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 5147	. 2 class R.
2		cnp 5139	. . . 4 class P.
3	2, 2	cxp 3249	. . 3 class (P. X. P.)
4		cer 5146	. . 3 class ~R
5	3, 4	cqs 4400	. 2 class ((P. X. P.)/. ~R )
6	1, 5	wceq 992	1 wff R. = ((P. X. P.)/. ~R )

This definition is referenced by:  srex 5333  addsrpr 5338  mulsrpr 5339  ltsrpr 5340  0nsr 5342  0r 5343  1r 5344  m1r 5345  addclsr 5346  mulclsr 5347  addcomsr 5350  addasssr 5351  mulcomsr 5352  mulasssr 5353  distrsr 5354  ltsosr 5357  0idsr 5360  1idsr 5361  00sr 5362  ltasr 5363  recexsrlem 5366  mulgt0sr 5368  map2psrpr 5374

Copyright terms: Public domain