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

Definition df-nr 6615
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  6633  mulsrpr  6634  ltsrprg  6635  gt0srpr  6636  0nsr  6637  0r  6638  1sr  6639  m1r  6640  addclsr  6641  mulclsr  6642  addcomsrg  6643  addasssrg  6644  mulcomsrg  6645  mulasssrg  6646  distrsrg  6647  lttrsr  6650  ltposr  6651  ltsosr  6652  0idsr  6655  1idsr  6656  00sr  6657  ltasrg  6658  recexgt0sr  6661  mulgt0sr  6664  aptisr  6665  mulextsr1  6667  archsr  6668  pitonnlem2  6703  axcnex  6705
  Copyright terms: Public domain W3C validator