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

Definition df-nr 6655
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  6673  mulsrpr  6674  ltsrprg  6675  gt0srpr  6676  0nsr  6677  0r  6678  1sr  6679  m1r  6680  addclsr  6681  mulclsr  6682  addcomsrg  6683  addasssrg  6684  mulcomsrg  6685  mulasssrg  6686  distrsrg  6687  lttrsr  6690  ltposr  6691  ltsosr  6692  0idsr  6695  1idsr  6696  00sr  6697  ltasrg  6698  recexgt0sr  6701  mulgt0sr  6704  aptisr  6705  mulextsr1  6707  archsr  6708  pitonnlem2  6743  axcnex  6745
  Copyright terms: Public domain W3C validator