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

Theorem ltnled 9176
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 9111 . 2  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  <  B  <->  -.  B  <_  A )
)
41, 2, 3syl2anc 643 1  |-  ( ph  ->  ( A  <  B  <->  -.  B  <_  A )
)
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177    e. wcel 1721   class class class wbr 4172   RRcr 8945    < clt 9076    <_ cle 9077
This theorem is referenced by:  ltsub1  9480  ltsub2  9481  fzodisj  11122  elfznelfzob  11148  sqrlem7  12009  sqrlt  12022  lo1bdd2  12273  isercoll  12416  fzm1ndvds  12856  fzo0dvdseq  12857  bitsfzolem  12901  bitsfzo  12902  sadcaddlem  12924  smuval2  12949  bezoutlem3  12995  isprm5  13067  odzdvds  13136  pc2dvds  13207  pockthg  13229  prmreclem1  13239  prmreclem5  13243  1arith  13250  4sqlem11  13278  vdwlem6  13309  vdwlem11  13314  ramlb  13342  oddvds  15140  gexdvds  15173  sylow1lem3  15189  coe1tmmul2  16623  zlpirlem3  16725  iccntr  18805  icccmplem2  18807  reconnlem2  18811  evth  18937  lebnumlem3  18941  nmoleub2lem3  19076  minveclem3b  19282  minveclem4  19286  pmltpclem2  19299  ovolgelb  19329  ovolicc2lem2  19367  ovolicc2lem4  19369  mbfposr  19497  itg2const2  19586  itg2cnlem2  19607  itg2cn  19608  plyco0  20064  coeeulem  20096  dgradd2  20139  pilem3  20322  cxplt2  20542  fsumharmonic  20803  ftalem3  20810  ftalem5  20812  ftalem7  20814  ppiprm  20887  chtprm  20889  chpub  20957  perfectlem2  20967  bposlem1  21021  lgsdilem2  21068  lgsqrlem2  21079  lgsquadlem2  21092  2sqblem  21114  pntpbnd1  21233  pntlem3  21256  eupath2lem3  21654  minvecolem4  22335  minvecolem5  22336  lmdvg  24291  ballotlemfc0  24703  ballotlemfcc  24704  ballotlemrv2  24732  dmlogdmgm  24761  lgamgulmlem1  24766  lgamucov  24775  erdszelem8  24837  fzp1nel  25163  fprodntriv  25221  mblfinlem  26143  itg2addnclem  26155  itg2addnclem2  26156  itg2addnclem3  26157  iblabsnclem  26167  dvreasin  26179  areacirclem5  26185  areacirclem6  26186  areacirc  26187  cntotbnd  26395  elpell1qr2  26825  pellfundglb  26838  pellfund14gap  26840  congabseq  26929  jm2.19  26954  jm2.26lem3  26962  dgraa0p  27222  stoweidlem26  27642  stoweidlem34  27650  stoweidlem59  27675  stirlinglem5  27694  0mnnnnn0  27971
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298  ax-pr 4363
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-ral 2671  df-rex 2672  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-br 4173  df-opab 4227  df-xp 4843  df-cnv 4845  df-xr 9080  df-le 9082
  Copyright terms: Public domain W3C validator