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

Definition df-lt 6724
Description: Define 'less than' on the real subset of complex numbers. (Contributed by NM, 22-Feb-1996.)
Assertion
Ref Expression
df-lt  <RR  { <. ,  >.  |  RR  RR  <. ,  0R >.  <. ,  0R >.  <R  }
Distinct variable group:   ,,,

Detailed syntax breakdown of Definition df-lt
StepHypRef Expression
1 cltrr 6715 . 2  <RR
2 vx . . . . . . 7  setvar
32cv 1241 . . . . . 6
4 cr 6710 . . . . . 6  RR
53, 4wcel 1390 . . . . 5  RR
6 vy . . . . . . 7  setvar
76cv 1241 . . . . . 6
87, 4wcel 1390 . . . . 5  RR
95, 8wa 97 . . . 4  RR  RR
10 vz . . . . . . . . . . 11  setvar
1110cv 1241 . . . . . . . . . 10
12 c0r 6282 . . . . . . . . . 10  0R
1311, 12cop 3370 . . . . . . . . 9  <. ,  0R >.
143, 13wceq 1242 . . . . . . . 8  <. ,  0R >.
15 vw . . . . . . . . . . 11  setvar
1615cv 1241 . . . . . . . . . 10
1716, 12cop 3370 . . . . . . . . 9  <. ,  0R >.
187, 17wceq 1242 . . . . . . . 8  <. ,  0R >.
1914, 18wa 97 . . . . . . 7  <. ,  0R >.  <. ,  0R >.
20 cltr 6287 . . . . . . . 8  <R
2111, 16, 20wbr 3755 . . . . . . 7  <R
2219, 21wa 97 . . . . . 6  <. ,  0R >.  <. ,  0R >.  <R
2322, 15wex 1378 . . . . 5  <. ,  0R >.  <. ,  0R >.  <R
2423, 10wex 1378 . . . 4  <. ,  0R >.  <. ,  0R >.  <R
259, 24wa 97 . . 3  RR  RR  <. ,  0R >.  <. ,  0R >.  <R
2625, 2, 6copab 3808 . 2  { <. ,  >.  |  RR  RR  <. ,  0R >.  <. ,  0R >.  <R  }
271, 26wceq 1242 1  <RR  { <. ,  >.  |  RR  RR  <. ,  0R >.  <. ,  0R >.  <R  }
Colors of variables: wff set class
This definition is referenced by:  ltrelre  6730  ltresr  6736
  Copyright terms: Public domain W3C validator