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

Theorem ltnled 9721
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 9653 . 2  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  <  B  <->  -.  B  <_  A )
)
41, 2, 3syl2anc 659 1  |-  ( ph  ->  ( A  <  B  <->  -.  B  <_  A )
)
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    e. wcel 1823   class class class wbr 4439   RRcr 9480    < clt 9617    <_ cle 9618
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pr 4676
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-rab 2813  df-v 3108  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-sn 4017  df-pr 4019  df-op 4023  df-br 4440  df-opab 4498  df-xp 4994  df-cnv 4996  df-xr 9621  df-le 9623
This theorem is referenced by:  ltsub1  10044  ltsub2  10045  0mnnnnn0  10824  fzp1nel  11766  fzodisj  11836  elfznelfzob  11897  swrdnd  12651  cshwcsh2id  12790  sqrlem7  13167  sqrtlt  13180  lo1bdd2  13432  isercoll  13575  fprodntriv  13834  fzm1ndvds  14125  fzo0dvdseq  14126  bitsfzolem  14171  bitsfzo  14172  sadcaddlem  14194  smuval2  14219  bezoutlem3  14265  isprm5  14340  odzdvds  14409  pc2dvds  14489  pockthg  14511  prmreclem1  14521  prmreclem5  14525  1arith  14532  4sqlem11  14560  vdwlem6  14591  vdwlem11  14596  ramlb  14624  oddvds  16773  gexdvds  16806  sylow1lem3  16822  coe1tmmul2  18515  zringlpirlem3  18702  iccntr  21495  icccmplem2  21497  reconnlem2  21501  evth  21628  lebnumlem3  21632  nmoleub2lem3  21767  minveclem3b  22012  minveclem4  22016  pmltpclem2  22030  ovolgelb  22060  ovolicc2lem2  22098  ovolicc2lem4  22100  mbfposr  22228  itg2const2  22317  itg2cnlem2  22338  itg2cn  22339  plyco0  22758  coeeulem  22790  dgradd2  22834  pilem3  23017  cxplt2  23250  fsumharmonic  23542  ftalem3  23549  ftalem5  23551  ftalem7  23553  ppiprm  23626  chtprm  23628  chpub  23696  perfectlem2  23706  bposlem1  23760  lgsdilem2  23807  lgsqrlem2  23818  lgsquadlem2  23831  2sqblem  23853  pntpbnd1  23972  pntlem3  23995  clwwlkgt0  24976  eupath2lem3  25184  frgrareggt1  25321  minvecolem4  25997  minvecolem5  25998  mul2lt0bi  27803  nndiffz1  27833  2sqmod  27873  lmdvg  28173  eulerpartlems  28566  ballotlemfc0  28698  ballotlemfcc  28699  ballotlemrv2  28727  signsply0  28775  dmlogdmgm  28833  lgamgulmlem1  28838  lgamucov  28847  erdszelem8  28909  mblfinlem2  30295  itg2addnclem  30309  itg2addnclem2  30310  itg2addnclem3  30311  iblabsnclem  30321  ftc1anclem5  30337  areacirclem4  30353  areacirclem5  30354  areacirc  30355  cntotbnd  30535  elpell1qr2  31050  pellfundglb  31063  pellfund14gap  31065  congabseq  31154  jm2.19  31177  jm2.26lem3  31185  dgraa0p  31342  dvgrat  31437  divlt0gt0d  31712  lptre2pt  31888  icccncfext  31932  ioodvbdlimc1lem2  31971  ioodvbdlimc2lem  31973  stoweidlem26  32050  stoweidlem34  32058  stoweidlem59  32083  stirlinglem5  32102  dirkercncflem1  32127  fourierdlem10  32141  fourierdlem19  32150  fourierdlem25  32156  fourierdlem35  32166  fourierdlem40  32171  fourierdlem42  32173  fourierdlem64  32195  fourierdlem65  32196  fourierdlem74  32205  fourierdlem75  32206  fourierdlem78  32209  fourierdlem79  32210  fourierdlem104  32235  fourierswlem  32255  fouriersw  32256  elaa2lem  32258  etransclem32  32291  etransclem41  32300  perfectALTVlem2  32616  aacllem  33623
  Copyright terms: Public domain W3C validator