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

Theorem ltnled 9184
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 9119 . 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 4180   RRcr 8953    < clt 9084    <_ cle 9085
This theorem is referenced by:  ltsub1  9488  ltsub2  9489  fzodisj  11130  elfznelfzob  11156  sqrlem7  12017  sqrlt  12030  lo1bdd2  12281  isercoll  12424  fzm1ndvds  12864  fzo0dvdseq  12865  bitsfzolem  12909  bitsfzo  12910  sadcaddlem  12932  smuval2  12957  bezoutlem3  13003  isprm5  13075  odzdvds  13144  pc2dvds  13215  pockthg  13237  prmreclem1  13247  prmreclem5  13251  1arith  13258  4sqlem11  13286  vdwlem6  13317  vdwlem11  13322  ramlb  13350  oddvds  15148  gexdvds  15181  sylow1lem3  15197  coe1tmmul2  16631  zlpirlem3  16733  iccntr  18813  icccmplem2  18815  reconnlem2  18819  evth  18945  lebnumlem3  18949  nmoleub2lem3  19084  minveclem3b  19290  minveclem4  19294  pmltpclem2  19307  ovolgelb  19337  ovolicc2lem2  19375  ovolicc2lem4  19377  mbfposr  19505  itg2const2  19594  itg2cnlem2  19615  itg2cn  19616  plyco0  20072  coeeulem  20104  dgradd2  20147  pilem3  20330  cxplt2  20550  fsumharmonic  20811  ftalem3  20818  ftalem5  20820  ftalem7  20822  ppiprm  20895  chtprm  20897  chpub  20965  perfectlem2  20975  bposlem1  21029  lgsdilem2  21076  lgsqrlem2  21087  lgsquadlem2  21100  2sqblem  21122  pntpbnd1  21241  pntlem3  21264  eupath2lem3  21662  minvecolem4  22343  minvecolem5  22344  lmdvg  24299  ballotlemfc0  24711  ballotlemfcc  24712  ballotlemrv2  24740  dmlogdmgm  24769  lgamgulmlem1  24774  lgamucov  24783  erdszelem8  24845  fzp1nel  25171  fprodntriv  25229  mblfinlem  26151  itg2addnclem  26163  itg2addnclem2  26164  itg2addnclem3  26165  iblabsnclem  26175  dvreasin  26187  areacirclem5  26193  areacirclem6  26194  areacirc  26195  cntotbnd  26403  elpell1qr2  26833  pellfundglb  26846  pellfund14gap  26848  congabseq  26937  jm2.19  26962  jm2.26lem3  26970  dgraa0p  27230  stoweidlem26  27650  stoweidlem34  27658  stoweidlem59  27683  stirlinglem5  27702  0mnnnnn0  27979
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 2393  ax-sep 4298  ax-nul 4306  ax-pr 4371
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 2266  df-mo 2267  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-ne 2577  df-ral 2679  df-rex 2680  df-rab 2683  df-v 2926  df-dif 3291  df-un 3293  df-in 3295  df-ss 3302  df-nul 3597  df-if 3708  df-sn 3788  df-pr 3789  df-op 3791  df-br 4181  df-opab 4235  df-xp 4851  df-cnv 4853  df-xr 9088  df-le 9090
  Copyright terms: Public domain W3C validator