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

Theorem ltnled 9807
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 9738 . 2  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  <  B  <->  -.  B  <_  A )
)
41, 2, 3syl2anc 671 1  |-  ( ph  ->  ( A  <  B  <->  -.  B  <_  A )
)
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 189    e. wcel 1897   class class class wbr 4415   RRcr 9563    < clt 9700    <_ cle 9701
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-9 1906  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441  ax-sep 4538  ax-nul 4547  ax-pr 4652
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-eu 2313  df-mo 2314  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ne 2634  df-ral 2753  df-rex 2754  df-rab 2757  df-v 3058  df-dif 3418  df-un 3420  df-in 3422  df-ss 3429  df-nul 3743  df-if 3893  df-sn 3980  df-pr 3982  df-op 3986  df-br 4416  df-opab 4475  df-xp 4858  df-cnv 4860  df-xr 9704  df-le 9706
This theorem is referenced by:  ltsub1  10137  ltsub2  10138  0mnnnnn0  10930  mul2lt0bi  11430  fzp1nel  11906  fzodisj  11982  elfznelfzob  12045  swrdnd  12824  cshwcsh2id  12963  sqrlem7  13360  sqrtlt  13373  lo1bdd2  13636  isercoll  13779  fprodntriv  14044  fzm1ndvds  14405  fzo0dvdseq  14406  bitsfzolem  14455  bitsfzolemOLD  14456  bitsfzo  14457  sadcaddlem  14479  smuval2  14504  bezoutlem3OLD  14553  bezoutlem3  14556  isprm5  14699  odzdvds  14788  odzdvdsOLD  14794  pc2dvds  14876  pockthg  14898  prmreclem1  14908  prmreclem5  14912  1arith  14919  4sqlem11  14947  vdwlem6  14984  vdwlem11  14989  ramlb  15025  oddvds  17244  gexdvds  17283  sylow1lem3  17300  coe1tmmul2  18917  zringlpirlem3OLD  19103  zringlpirlem3  19105  iccntr  21887  icccmplem2  21889  reconnlem2  21893  evth  22035  lebnumlem3  22039  lebnumlem3OLD  22042  nmoleub2lem3  22177  minveclem3b  22418  minveclem4  22422  minveclem3bOLD  22430  minveclem4OLD  22434  pmltpclem2  22448  ovolgelb  22481  ovolicc2lem2  22519  ovolicc2lem4OLD  22521  ovolicc2lem4  22522  mbfposr  22656  itg2const2  22747  itg2cnlem2  22768  itg2cn  22769  plyco0  23194  coeeulem  23226  dgradd2  23270  pilem3  23457  pilem3OLD  23458  cxplt2  23691  fsumharmonic  23985  dmlogdmgm  23997  lgamgulmlem1  24002  lgamucov  24011  ftalem3  24047  ftalem5  24049  ftalem5OLD  24051  ftalem7  24053  ppiprm  24126  chtprm  24128  chpub  24196  perfectlem2  24206  bposlem1  24260  lgsdilem2  24307  lgsqrlem2  24318  lgsquadlem2  24331  2sqblem  24353  pntpbnd1  24472  pntlem3  24495  clwwlkgt0  25547  eupath2lem3  25755  frgrareggt1  25892  minvecolem4  26570  minvecolem5  26571  minvecolem4OLD  26580  minvecolem5OLD  26581  nndiffz1  28414  2sqmod  28457  psgnfzto1stlem  28661  lmdvg  28807  eulerpartlems  29241  ballotlemfc0  29373  ballotlemfcc  29374  ballotlemrv2  29402  ballotlemrv2OLD  29440  signsply0  29488  erdszelem8  29969  bccolsum  30423  poimirlem2  31986  poimirlem3  31987  poimirlem6  31990  poimirlem7  31991  poimirlem8  31992  poimirlem16  32000  poimirlem17  32001  poimirlem19  32003  poimirlem20  32004  poimirlem21  32005  poimirlem22  32006  poimirlem23  32007  poimirlem26  32010  poimirlem31  32015  poimir  32017  mblfinlem2  32022  itg2addnclem  32037  itg2addnclem2  32038  itg2addnclem3  32039  iblabsnclem  32049  ftc1anclem5  32065  areacirclem4  32079  areacirclem5  32080  areacirc  32081  cntotbnd  32172  elpell1qr2  35762  pellfundglb  35777  pellfund14gap  35779  congabseq  35868  jm2.19  35892  jm2.26lem3  35900  dgraa0p  36059  dvgrat  36704  uzwo4  37429  divlt0gt0d  37533  supxrgere  37593  lptre2pt  37757  icccncfext  37802  ioodvbdlimc1lem2  37841  ioodvbdlimc1lem2OLD  37843  ioodvbdlimc2lem  37845  ioodvbdlimc2lemOLD  37846  stoweidlem26  37923  stoweidlem34  37932  stoweidlem59  37957  stirlinglem5  37977  dirkercncflem1  38002  fourierdlem10  38016  fourierdlem19  38025  fourierdlem25  38031  fourierdlem35  38042  fourierdlem40  38047  fourierdlem42  38049  fourierdlem42OLD  38050  fourierdlem64  38071  fourierdlem65  38072  fourierdlem74  38081  fourierdlem75  38082  fourierdlem78  38085  fourierdlem79  38086  fourierdlem104  38111  fourierswlem  38131  fouriersw  38132  elaa2lem  38134  elaa2lemOLD  38135  etransclem32  38168  etransclem41  38177  hsphoidmvle2  38444  hoidmv1lelem1  38450  hoidmv1lelem2  38451  hoidmv1lelem3  38452  hoidmvlelem2  38455  hoidmvlelem4  38457  hoidmvlelem5  38458  hoiqssbllem3  38483  hspmbllem1  38485  hspmbllem2  38486  perfectALTVlem2  38881  nbusgrvtxm1  39502  aacllem  40812
  Copyright terms: Public domain W3C validator