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

Theorem ltnled 9517
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 9450 . 2  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  <  B  <->  -.  B  <_  A )
)
41, 2, 3syl2anc 656 1  |-  ( ph  ->  ( A  <  B  <->  -.  B  <_  A )
)
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    e. wcel 1761   class class class wbr 4289   RRcr 9277    < clt 9414    <_ cle 9415
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-9 1765  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-sep 4410  ax-nul 4418  ax-pr 4528
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-eu 2261  df-mo 2262  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-ral 2718  df-rex 2719  df-rab 2722  df-v 2972  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-nul 3635  df-if 3789  df-sn 3875  df-pr 3877  df-op 3881  df-br 4290  df-opab 4348  df-xp 4842  df-cnv 4844  df-xr 9418  df-le 9420
This theorem is referenced by:  ltsub1  9831  ltsub2  9832  0mnnnnn0  10608  fzodisj  11579  elfznelfzob  11627  sqrlem7  12734  sqrlt  12747  lo1bdd2  12998  isercoll  13141  fzm1ndvds  13581  fzo0dvdseq  13582  bitsfzolem  13626  bitsfzo  13627  sadcaddlem  13649  smuval2  13674  bezoutlem3  13720  isprm5  13794  odzdvds  13863  pc2dvds  13941  pockthg  13963  prmreclem1  13973  prmreclem5  13977  1arith  13984  4sqlem11  14012  vdwlem6  14043  vdwlem11  14048  ramlb  14076  oddvds  16043  gexdvds  16076  sylow1lem3  16092  coe1tmmul2  17704  zringlpirlem3  17864  zlpirlem3  17869  iccntr  20357  icccmplem2  20359  reconnlem2  20363  evth  20490  lebnumlem3  20494  nmoleub2lem3  20629  minveclem3b  20874  minveclem4  20878  pmltpclem2  20892  ovolgelb  20922  ovolicc2lem2  20960  ovolicc2lem4  20962  mbfposr  21089  itg2const2  21178  itg2cnlem2  21199  itg2cn  21200  plyco0  21619  coeeulem  21651  dgradd2  21694  pilem3  21877  cxplt2  22102  fsumharmonic  22364  ftalem3  22371  ftalem5  22373  ftalem7  22375  ppiprm  22448  chtprm  22450  chpub  22518  perfectlem2  22528  bposlem1  22582  lgsdilem2  22629  lgsqrlem2  22640  lgsquadlem2  22653  2sqblem  22675  pntpbnd1  22794  pntlem3  22817  eupath2lem3  23535  minvecolem4  24216  minvecolem5  24217  mul2lt0bi  25977  nndiffz1  26008  lmdvg  26319  eulerpartlems  26673  ballotlemfc0  26805  ballotlemfcc  26806  ballotlemrv2  26834  signsply0  26882  dmlogdmgm  26940  lgamgulmlem1  26945  lgamucov  26954  erdszelem8  27016  fzp1nel  27326  fprodntriv  27384  mblfinlem2  28354  itg2addnclem  28368  itg2addnclem2  28369  itg2addnclem3  28370  iblabsnclem  28380  ftc1anclem5  28396  areacirclem4  28412  areacirclem5  28413  areacirc  28414  cntotbnd  28620  elpell1qr2  29138  pellfundglb  29151  pellfund14gap  29153  congabseq  29242  jm2.19  29267  jm2.26lem3  29275  dgraa0p  29431  stoweidlem26  29746  stoweidlem34  29754  stoweidlem59  29779  stirlinglem5  29798  clwwlkgt0  30359  erclwwlktr0  30404  frgrareggt1  30634
  Copyright terms: Public domain W3C validator