MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-lt Unicode version

Definition df-lt 9526
Description: Define 'less than' on the real subset of complex numbers. Proofs should typically use instead; see df-ltxr 9654. (Contributed by NM, 22-Feb-1996.) (New usage is discouraged.)
Assertion
Ref Expression
df-lt
Distinct variable group:   , , ,

Detailed syntax breakdown of Definition df-lt
StepHypRef Expression
1 cltrr 9517 . 2
2 vx . . . . . . 7
32cv 1394 . . . . . 6
4 cr 9512 . . . . . 6
53, 4wcel 1818 . . . . 5
6 vy . . . . . . 7
76cv 1394 . . . . . 6
87, 4wcel 1818 . . . . 5
95, 8wa 369 . . . 4
10 vz . . . . . . . . . . 11
1110cv 1394 . . . . . . . . . 10
12 c0r 9265 . . . . . . . . . 10
1311, 12cop 4035 . . . . . . . . 9
143, 13wceq 1395 . . . . . . . 8
15 vw . . . . . . . . . . 11
1615cv 1394 . . . . . . . . . 10
1716, 12cop 4035 . . . . . . . . 9
187, 17wceq 1395 . . . . . . . 8
1914, 18wa 369 . . . . . . 7
20 cltr 9270 . . . . . . . 8
2111, 16, 20wbr 4452 . . . . . . 7
2219, 21wa 369 . . . . . 6
2322, 15wex 1612 . . . . 5
2423, 10wex 1612 . . . 4
259, 24wa 369 . . 3
2625, 2, 6copab 4509 . 2
271, 26wceq 1395 1
Colors of variables: wff setvar class
This definition is referenced by:  ltrelre  9532  ltresr  9538
  Copyright terms: Public domain W3C validator