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

Theorem ltnlei 9736
Description: 'Less than' in terms of 'less than or equal to'. (Contributed by NM, 11-Jul-2005.)
Hypotheses
Ref Expression
lt.1  |-  A  e.  RR
lt.2  |-  B  e.  RR
Assertion
Ref Expression
ltnlei  |-  ( A  <  B  <->  -.  B  <_  A )

Proof of Theorem ltnlei
StepHypRef Expression
1 lt.2 . . 3  |-  B  e.  RR
2 lt.1 . . 3  |-  A  e.  RR
31, 2lenlti 9735 . 2  |-  ( B  <_  A  <->  -.  A  <  B )
43con2bii 330 1  |-  ( A  <  B  <->  -.  B  <_  A )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 184    e. wcel 1842   class class class wbr 4394   RRcr 9520    < clt 9657    <_ cle 9658
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-sep 4516  ax-nul 4524  ax-pr 4629
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-ral 2758  df-rex 2759  df-rab 2762  df-v 3060  df-dif 3416  df-un 3418  df-in 3420  df-ss 3427  df-nul 3738  df-if 3885  df-sn 3972  df-pr 3974  df-op 3978  df-br 4395  df-opab 4453  df-xp 4828  df-cnv 4830  df-xr 9661  df-le 9663
This theorem is referenced by:  letrii  9740  nn0ge2m1nn  10901  zgt1rpn0n1  11302  fzpreddisj  11782  hashnn0n0nn  12505  hashge2el2dif  12568  n2dvds1  14242  divalglem5  14262  divalglem6  14263  sadcadd  14315  strlemor1  14934  htpycc  21770  pco1  21805  pcohtpylem  21809  pcopt  21812  pcopt2  21813  pcoass  21814  pcorevlem  21816  vitalilem5  22311  vieta1lem2  22997  ppiltx  23830  ppiublem1  23856  chtub  23866  axlowdimlem16  24664  axlowdim  24668  spthispth  24979  ballotlem2  28919  subfacp1lem1  29463  subfacp1lem5  29468  bcneg1  29932  fdc  31500  pellexlem6  35111  jm2.23  35280
  Copyright terms: Public domain W3C validator