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

Theorem ltnled 9733
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 9664 . 2  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  <  B  <->  -.  B  <_  A )
)
41, 2, 3syl2anc 665 1  |-  ( ph  ->  ( A  <  B  <->  -.  B  <_  A )
)
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 187    e. wcel 1872   class class class wbr 4366   RRcr 9489    < clt 9626    <_ cle 9627
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408  ax-sep 4489  ax-nul 4498  ax-pr 4603
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2280  df-mo 2281  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-ne 2601  df-ral 2719  df-rex 2720  df-rab 2723  df-v 3024  df-dif 3382  df-un 3384  df-in 3386  df-ss 3393  df-nul 3705  df-if 3855  df-sn 3942  df-pr 3944  df-op 3948  df-br 4367  df-opab 4426  df-xp 4802  df-cnv 4804  df-xr 9630  df-le 9632
This theorem is referenced by:  ltsub1  10061  ltsub2  10062  0mnnnnn0  10853  mul2lt0bi  11353  fzp1nel  11829  fzodisj  11903  elfznelfzob  11965  swrdnd  12734  cshwcsh2id  12873  sqrlem7  13256  sqrtlt  13269  lo1bdd2  13531  isercoll  13674  fprodntriv  13939  fzm1ndvds  14300  fzo0dvdseq  14301  bitsfzolem  14350  bitsfzolemOLD  14351  bitsfzo  14352  sadcaddlem  14374  smuval2  14399  bezoutlem3OLD  14448  bezoutlem3  14451  isprm5  14594  odzdvds  14683  odzdvdsOLD  14689  pc2dvds  14771  pockthg  14793  prmreclem1  14803  prmreclem5  14807  1arith  14814  4sqlem11  14842  vdwlem6  14879  vdwlem11  14884  ramlb  14920  oddvds  17139  gexdvds  17178  sylow1lem3  17195  coe1tmmul2  18812  zringlpirlem3OLD  18997  zringlpirlem3  18999  iccntr  21781  icccmplem2  21783  reconnlem2  21787  evth  21929  lebnumlem3  21933  lebnumlem3OLD  21936  nmoleub2lem3  22071  minveclem3b  22312  minveclem4  22316  minveclem3bOLD  22324  minveclem4OLD  22328  pmltpclem2  22342  ovolgelb  22375  ovolicc2lem2  22413  ovolicc2lem4OLD  22415  ovolicc2lem4  22416  mbfposr  22550  itg2const2  22641  itg2cnlem2  22662  itg2cn  22663  plyco0  23088  coeeulem  23120  dgradd2  23164  pilem3  23351  pilem3OLD  23352  cxplt2  23585  fsumharmonic  23879  dmlogdmgm  23891  lgamgulmlem1  23896  lgamucov  23905  ftalem3  23941  ftalem5  23943  ftalem5OLD  23945  ftalem7  23947  ppiprm  24020  chtprm  24022  chpub  24090  perfectlem2  24100  bposlem1  24154  lgsdilem2  24201  lgsqrlem2  24212  lgsquadlem2  24225  2sqblem  24247  pntpbnd1  24366  pntlem3  24389  clwwlkgt0  25441  eupath2lem3  25649  frgrareggt1  25786  minvecolem4  26464  minvecolem5  26465  minvecolem4OLD  26474  minvecolem5OLD  26475  nndiffz1  28316  2sqmod  28360  psgnfzto1stlem  28565  lmdvg  28711  eulerpartlems  29145  ballotlemfc0  29277  ballotlemfcc  29278  ballotlemrv2  29306  ballotlemrv2OLD  29344  signsply0  29392  erdszelem8  29873  bccolsum  30326  poimirlem2  31849  poimirlem3  31850  poimirlem6  31853  poimirlem7  31854  poimirlem8  31855  poimirlem16  31863  poimirlem17  31864  poimirlem19  31866  poimirlem20  31867  poimirlem21  31868  poimirlem22  31869  poimirlem23  31870  poimirlem26  31873  poimirlem31  31878  poimir  31880  mblfinlem2  31885  itg2addnclem  31900  itg2addnclem2  31901  itg2addnclem3  31902  iblabsnclem  31912  ftc1anclem5  31928  areacirclem4  31942  areacirclem5  31943  areacirc  31944  cntotbnd  32035  elpell1qr2  35631  pellfundglb  35646  pellfund14gap  35648  congabseq  35737  jm2.19  35761  jm2.26lem3  35769  dgraa0p  35928  dvgrat  36574  uzwo4  37308  divlt0gt0d  37393  supxrgere  37453  lptre2pt  37603  icccncfext  37648  ioodvbdlimc1lem2  37687  ioodvbdlimc1lem2OLD  37689  ioodvbdlimc2lem  37691  ioodvbdlimc2lemOLD  37692  stoweidlem26  37769  stoweidlem34  37778  stoweidlem59  37803  stirlinglem5  37823  dirkercncflem1  37848  fourierdlem10  37862  fourierdlem19  37871  fourierdlem25  37877  fourierdlem35  37888  fourierdlem40  37893  fourierdlem42  37895  fourierdlem42OLD  37896  fourierdlem64  37917  fourierdlem65  37918  fourierdlem74  37927  fourierdlem75  37928  fourierdlem78  37931  fourierdlem79  37932  fourierdlem104  37957  fourierswlem  37977  fouriersw  37978  elaa2lem  37980  elaa2lemOLD  37981  etransclem32  38014  etransclem41  38023  hsphoidmvle2  38254  hoidmv1lelem1  38260  hoidmv1lelem2  38261  hoidmv1lelem3  38262  hoidmvlelem2  38265  hoidmvlelem4  38267  hoidmvlelem5  38268  perfectALTVlem2  38657  aacllem  40143
  Copyright terms: Public domain W3C validator