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

Theorem ltnled 9727
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 9660 . 2  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  <  B  <->  -.  B  <_  A )
)
41, 2, 3syl2anc 661 1  |-  ( ph  ->  ( A  <  B  <->  -.  B  <_  A )
)
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    e. wcel 1767   class class class wbr 4447   RRcr 9487    < clt 9624    <_ cle 9625
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pr 4686
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-br 4448  df-opab 4506  df-xp 5005  df-cnv 5007  df-xr 9628  df-le 9630
This theorem is referenced by:  ltsub1  10044  ltsub2  10045  0mnnnnn0  10824  fzodisj  11823  elfznelfzob  11880  cshwcsh2id  12755  sqrlem7  13041  sqrtlt  13054  lo1bdd2  13306  isercoll  13449  fzm1ndvds  13893  fzo0dvdseq  13894  bitsfzolem  13939  bitsfzo  13940  sadcaddlem  13962  smuval2  13987  bezoutlem3  14033  isprm5  14108  odzdvds  14177  pc2dvds  14257  pockthg  14279  prmreclem1  14289  prmreclem5  14293  1arith  14300  4sqlem11  14328  vdwlem6  14359  vdwlem11  14364  ramlb  14392  oddvds  16367  gexdvds  16400  sylow1lem3  16416  coe1tmmul2  18088  zringlpirlem3  18278  zlpirlem3  18283  iccntr  21061  icccmplem2  21063  reconnlem2  21067  evth  21194  lebnumlem3  21198  nmoleub2lem3  21333  minveclem3b  21578  minveclem4  21582  pmltpclem2  21596  ovolgelb  21626  ovolicc2lem2  21664  ovolicc2lem4  21666  mbfposr  21794  itg2const2  21883  itg2cnlem2  21904  itg2cn  21905  plyco0  22324  coeeulem  22356  dgradd2  22399  pilem3  22582  cxplt2  22807  fsumharmonic  23069  ftalem3  23076  ftalem5  23078  ftalem7  23080  ppiprm  23153  chtprm  23155  chpub  23223  perfectlem2  23233  bposlem1  23287  lgsdilem2  23334  lgsqrlem2  23345  lgsquadlem2  23358  2sqblem  23380  pntpbnd1  23499  pntlem3  23522  clwwlkgt0  24447  eupath2lem3  24655  frgrareggt1  24793  minvecolem4  25472  minvecolem5  25473  mul2lt0bi  27237  nndiffz1  27264  lmdvg  27571  eulerpartlems  27939  ballotlemfc0  28071  ballotlemfcc  28072  ballotlemrv2  28100  signsply0  28148  dmlogdmgm  28206  lgamgulmlem1  28211  lgamucov  28220  erdszelem8  28282  fzp1nel  28593  fprodntriv  28651  mblfinlem2  29629  itg2addnclem  29643  itg2addnclem2  29644  itg2addnclem3  29645  iblabsnclem  29655  ftc1anclem5  29671  areacirclem4  29687  areacirclem5  29688  areacirc  29689  cntotbnd  29895  elpell1qr2  30412  pellfundglb  30425  pellfund14gap  30427  congabseq  30516  jm2.19  30539  jm2.26lem3  30547  dgraa0p  30703  lptre2pt  31182  icccncfext  31226  ioodvbdlimc1lem2  31262  ioodvbdlimc2lem  31264  stoweidlem26  31326  stoweidlem34  31334  stoweidlem59  31359  stirlinglem5  31378  fourierdlem10  31417  fourierdlem19  31426  fourierdlem25  31432  fourierdlem35  31442  fourierdlem40  31447  fourierdlem42  31449  fourierdlem64  31471  fourierdlem65  31472  fourierdlem74  31481  fourierdlem75  31482  fourierdlem78  31485  fourierdlem79  31486  fourierdlem104  31511  fourierdlem107  31514  fourierswlem  31531  fouriersw  31532
  Copyright terms: Public domain W3C validator