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

Theorem ltnlei 9029
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 9028 . 2  |-  ( B  <_  A  <->  -.  A  <  B )
43con2bii 322 1  |-  ( A  <  B  <->  -.  B  <_  A )
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 176    e. wcel 1710   class class class wbr 4104   RRcr 8826    < clt 8957    <_ cle 8958
This theorem is referenced by:  letrii  9034  divalglem5  12693  divalglem6  12694  bitsfzolem  12722  bitsfzo  12723  bitsinv1lem  12729  sadcadd  12746  strlemor1  13332  htpycc  18582  pco1  18617  pcohtpylem  18621  pcopt  18624  pcopt2  18625  pcoass  18626  pcorevlem  18628  vitalilem5  19071  vieta1lem2  19795  ppiltx  20527  ppiublem1  20553  chtub  20563  rnlogblem  23665  ballotlem2  23995  subfacp1lem1  24114  subfacp1lem5  24119  axlowdimlem16  25144  axlowdim  25148  fdc  25779  pellexlem6  26242  jm2.23  26412  hashnn0n0nn  27495  spthispth  27715
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339  ax-sep 4222  ax-nul 4230  ax-pr 4295
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2213  df-mo 2214  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ne 2523  df-ral 2624  df-rex 2625  df-rab 2628  df-v 2866  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-nul 3532  df-if 3642  df-sn 3722  df-pr 3723  df-op 3725  df-br 4105  df-opab 4159  df-xp 4777  df-cnv 4779  df-xr 8961  df-le 8963
  Copyright terms: Public domain W3C validator