ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-nr Structured version   GIF version

Definition df-nr 6635
Description: Define class of signed reals. This is a "temporary" set used in the construction of complex numbers, and is intended to be used only by the construction. From Proposition 9-4.2 of [Gleason] p. 126. (Contributed by NM, 25-Jul-1995.)
Assertion
Ref Expression
df-nr R = ((P × P) / ~R )

Detailed syntax breakdown of Definition df-nr
StepHypRef Expression
1 cnr 6281 . 2 class R
2 cnp 6275 . . . 4 class P
32, 2cxp 4286 . . 3 class (P × P)
4 cer 6280 . . 3 class ~R
53, 4cqs 6041 . 2 class ((P × P) / ~R )
61, 5wceq 1242 1 wff R = ((P × P) / ~R )
Colors of variables: wff set class
This definition is referenced by:  addsrpr  6653  mulsrpr  6654  ltsrprg  6655  gt0srpr  6656  0nsr  6657  0r  6658  1sr  6659  m1r  6660  addclsr  6661  mulclsr  6662  addcomsrg  6663  addasssrg  6664  mulcomsrg  6665  mulasssrg  6666  distrsrg  6667  lttrsr  6670  ltposr  6671  ltsosr  6672  0idsr  6675  1idsr  6676  00sr  6677  ltasrg  6678  recexgt0sr  6681  mulgt0sr  6684  aptisr  6685  mulextsr1  6687  archsr  6688  pitonnlem2  6723  axcnex  6725
  Copyright terms: Public domain W3C validator