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

Theorem ltnled 9056
Description: 'Less than' in terms of 'less than or equal to'. (Contributed by Mario Carneiro, 27-May-2016.)
Hypotheses
Ref Expression
ltd.1  |-  ( ph  ->  A  e.  RR )
ltd.2  |-  ( ph  ->  B  e.  RR )
Assertion
Ref Expression
ltnled  |-  ( ph  ->  ( A  <  B  <->  -.  B  <_  A )
)

Proof of Theorem ltnled
StepHypRef Expression
1 ltd.1 . 2  |-  ( ph  ->  A  e.  RR )
2 ltd.2 . 2  |-  ( ph  ->  B  e.  RR )
3 ltnle 8992 . 2  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  <  B  <->  -.  B  <_  A )
)
41, 2, 3syl2anc 642 1  |-  ( ph  ->  ( A  <  B  <->  -.  B  <_  A )
)
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    e. wcel 1710   class class class wbr 4104   RRcr 8826    < clt 8957    <_ cle 8958
This theorem is referenced by:  ltsub1  9360  ltsub2  9361  fzodisj  10992  sqrlem7  11830  sqrlt  11843  lo1bdd2  12094  isercoll  12237  fzm1ndvds  12677  fzo0dvdseq  12678  bitsfzolem  12722  bitsfzo  12723  sadcaddlem  12745  smuval2  12770  bezoutlem3  12816  isprm5  12888  odzdvds  12957  pc2dvds  13028  pockthg  13050  prmreclem1  13060  prmreclem5  13064  1arith  13071  4sqlem11  13099  vdwlem6  13130  vdwlem11  13135  ramlb  13163  oddvds  14961  gexdvds  14994  sylow1lem3  15010  coe1tmmul2  16451  zlpirlem3  16549  iccntr  18429  icccmplem2  18431  reconnlem2  18435  evth  18561  lebnumlem3  18565  nmoleub2lem3  18700  minveclem3b  18896  minveclem4  18900  pmltpclem2  18913  ovolgelb  18943  ovolicc2lem2  18981  ovolicc2lem4  18983  mbfposr  19111  itg2const2  19200  itg2cnlem2  19221  itg2cn  19222  plyco0  19678  coeeulem  19710  dgradd2  19753  pilem3  19936  cxplt2  20156  fsumharmonic  20417  ftalem3  20424  ftalem5  20426  ftalem7  20428  ppiprm  20501  chtprm  20503  chpub  20571  perfectlem2  20581  bposlem1  20635  lgsdilem2  20682  lgsqrlem2  20693  lgsquadlem2  20706  2sqblem  20728  pntpbnd1  20847  pntlem3  20870  minvecolem4  21573  minvecolem5  21574  lmdvg  23494  ballotlemfc0  23999  ballotlemfcc  24000  ballotlemrv2  24028  dmlogdmgm  24057  lgamgulmlem1  24062  lgamucov  24071  erdszelem8  24133  eupath2lem3  24307  fzp1nel  24511  fprodntriv  24569  itg2addnclem  25492  itg2addnclem2  25493  itg2addnc  25494  iblabsnclem  25503  dvreasin  25515  areacirclem5  25521  areacirclem6  25522  areacirc  25523  cntotbnd  25843  elpell1qr2  26280  pellfundglb  26293  pellfund14gap  26295  congabseq  26384  jm2.19  26409  jm2.26lem3  26417  dgraa0p  26677  stoweidlem59  27131  stirlinglem5  27150  elfznelfzob  27463
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