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

Theorem ltnlei 9154
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 9153 . 2  |-  ( B  <_  A  <->  -.  A  <  B )
43con2bii 323 1  |-  ( A  <  B  <->  -.  B  <_  A )
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 177    e. wcel 1721   class class class wbr 4176   RRcr 8949    < clt 9080    <_ cle 9081
This theorem is referenced by:  letrii  9158  hashnn0n0nn  11623  divalglem5  12876  divalglem6  12877  bitsfzolem  12905  bitsfzo  12906  bitsinv1lem  12912  sadcadd  12929  strlemor1  13515  htpycc  18962  pco1  18997  pcohtpylem  19001  pcopt  19004  pcopt2  19005  pcoass  19006  pcorevlem  19008  vitalilem5  19461  vieta1lem2  20185  ppiltx  20917  ppiublem1  20943  chtub  20953  spthispth  21530  rnlogblem  24356  ballotlem2  24703  subfacp1lem1  24822  subfacp1lem5  24827  axlowdimlem16  25804  axlowdim  25808  fdc  26343  pellexlem6  26791  jm2.23  26961
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2389  ax-sep 4294  ax-nul 4302  ax-pr 4367
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2262  df-mo 2263  df-clab 2395  df-cleq 2401  df-clel 2404  df-nfc 2533  df-ne 2573  df-ral 2675  df-rex 2676  df-rab 2679  df-v 2922  df-dif 3287  df-un 3289  df-in 3291  df-ss 3298  df-nul 3593  df-if 3704  df-sn 3784  df-pr 3785  df-op 3787  df-br 4177  df-opab 4231  df-xp 4847  df-cnv 4849  df-xr 9084  df-le 9086
  Copyright terms: Public domain W3C validator