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

Theorem lelttric 9427
Description: Trichotomy law. (Contributed by NM, 4-Apr-2005.)
Assertion
Ref Expression
lelttric

Proof of Theorem lelttric
StepHypRef Expression
1 pm2.1 410 . 2
2 lenlt 9399 . . 3
32orbi1d 687 . 2
41, 3mpbiri 227 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  \/wo 361  /\wa 362  e.wcel 1749   class class class wbr 4267   cr 9227   clt 9364   cle 9365
This theorem is referenced by:  ltlecasei  9428  fzsplit2  11418  uzsplit  11471  fzospliti  11522  fzouzsplit  11525  discr1  11941  faclbnd  12007  faclbnd4lem1  12010  faclbnd4lem4  12013  dvdslelem  13517  icccmplem2  20100  icccmp  20102  bcmono  22357  bpos1lem  22362  bposlem3  22366  bpos  22373  fzsplit3  25756  lzunuz  28779  jm2.24  28979
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1586  ax-4 1597  ax-5 1661  ax-6 1701  ax-7 1721  ax-9 1753  ax-10 1768  ax-11 1773  ax-12 1785  ax-13 1934  ax-ext 2403  ax-sep 4388  ax-nul 4396  ax-pr 4503
This theorem depends on definitions:  df-bi 179  df-or 363  df-an 364  df-3an 952  df-tru 1355  df-ex 1582  df-nf 1585  df-sb 1694  df-eu 2248  df-mo 2249  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2547  df-ne 2587  df-ral 2699  df-rex 2700  df-rab 2703  df-v 2953  df-dif 3308  df-un 3310  df-in 3312  df-ss 3319  df-nul 3615  df-if 3769  df-sn 3859  df-pr 3860  df-op 3862  df-br 4268  df-opab 4326  df-xp 4817  df-cnv 4819  df-xr 9368  df-le 9370
  Copyright terms: Public domain W3C validator