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

Theorem ltled 9185
Description: 'Less than' implies '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 )
ltled.1  |-  ( ph  ->  A  <  B )
Assertion
Ref Expression
ltled  |-  ( ph  ->  A  <_  B )

Proof of Theorem ltled
StepHypRef Expression
1 ltled.1 . 2  |-  ( ph  ->  A  <  B )
2 ltd.1 . . 3  |-  ( ph  ->  A  e.  RR )
3 ltd.2 . . 3  |-  ( ph  ->  B  e.  RR )
4 ltle 9127 . . 3  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  <  B  ->  A  <_  B )
)
52, 3, 4syl2anc 643 . 2  |-  ( ph  ->  ( A  <  B  ->  A  <_  B )
)
61, 5mpd 15 1  |-  ( ph  ->  A  <_  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1721   class class class wbr 4180   RRcr 8953    < clt 9084    <_ cle 9085
This theorem is referenced by:  ltnsymd  9186  mulge0  9509  msqge0  9513  addgt0d  9565  lt2addd  9612  lt2msq1  9857  uzwo3  10533  expmulnbnd  11474  fzsdom2  11656  isercolllem1  12421  caucvgrlem  12429  climcnds  12594  geomulcvg  12616  mertenslem1  12624  ruclem2  12794  ruclem12  12803  bitsfzo  12910  bitsmod  12911  4sqlem7  13275  vdwlem1  13312  met1stc  18512  cfilucfilOLD  18560  cfilucfil  18561  nlmvscnlem2  18682  icccmplem2  18815  reconnlem2  18819  xrhmeo  18932  cnheibor  18941  nmoleub2lem3  19084  ipcnlem2  19159  minveclem3b  19290  ivthlem1  19309  ivthlem2  19310  ivth2  19313  ivthle  19314  ivthle2  19315  ovollb2lem  19345  ovolicc2lem4  19377  ovolicc2lem5  19378  ioombl1lem4  19416  uniioombllem4  19439  uniioombllem5  19440  opnmbllem  19454  ismbf3d  19507  mbfi1fseqlem6  19573  itg2gt0  19613  dveflem  19824  dvferm1lem  19829  dvferm2lem  19831  rollelem  19834  rolle  19835  cmvth  19836  mvth  19837  c1liplem1  19841  dvgt0lem1  19847  dvivthlem1  19853  lhop1lem  19858  lhop1  19859  dvcnvrelem1  19862  dvcnvrelem2  19863  dvcvx  19865  dgradd2  20147  aaliou3lem8  20223  aaliou3lem7  20227  ulmdvlem1  20277  itgulm  20285  radcnvlt1  20295  radcnvle  20297  abelthlem7  20315  efcvx  20326  coseq0negpitopi  20372  tangtx  20374  tanabsge  20375  tanord  20401  abslogimle  20432  divlogrlim  20487  logno1  20488  logcnlem3  20496  logcnlem4  20497  logtayl  20512  logccv  20515  cxple  20547  chordthmlem4  20637  asinsin  20693  atanlogaddlem  20714  atantan  20724  cxp2limlem  20775  logdifbnd  20793  emcllem4  20798  harmonicbnd4  20810  ftalem1  20816  ftalem2  20817  ftalem3  20818  basellem5  20828  basellem8  20831  chpchtsum  20964  bposlem1  21029  lgseisenlem1  21094  lgsquadlem1  21099  lgsquadlem2  21100  lgsquadlem3  21101  chebbnd1lem2  21125  chebbnd1lem3  21126  chtppilimlem1  21128  chto1ub  21131  chpo1ubb  21136  vmadivsumb  21138  dchrisumlem3  21146  mulog2sumlem1  21189  vmalogdivsum2  21193  vmalogdivsum  21194  2vmadivsumlem  21195  selbergb  21204  selberg2b  21207  chpdifbndlem1  21208  selberg3lem2  21213  selberg3  21214  selberg4lem1  21215  selberg4  21216  pntrsumbnd  21221  selberg3r  21224  selberg4r  21225  selberg34r  21226  pntrlog2bndlem1  21232  pntrlog2bndlem2  21233  pntrlog2bndlem3  21234  pntrlog2bndlem4  21235  pntrlog2bndlem5  21236  pntrlog2bndlem6a  21237  pntrlog2bndlem6  21238  pntrlog2bnd  21239  pntpbnd1a  21240  pntpbnd1  21241  pntpbnd2  21242  pntibndlem2  21246  pntlemb  21252  pntlemq  21256  pntlemr  21257  pntlemj  21258  pntlemf  21260  pntlemp  21265  ostth2lem2  21289  smcnlem  22154  bcm1n  24112  dya2icoseg  24588  dstfrvunirn  24693  ballotlemfc0  24711  ballotlemfcc  24712  ballotlemimin  24724  ballotlemsgt1  24729  ballotlemfrcn0  24748  lgamucov  24783  subfacval3  24836  erdszelem8  24845  cvmliftlem6  24938  cvmliftlem7  24939  cvmliftlem8  24940  cvmliftlem9  24941  cvmliftlem10  24942  sinccvglem  25070  fznatpl1  25159  axpaschlem  25791  axlowdimlem16  25808  lxflflp1  26150  mblfinlem  26151  itg2addnclem  26163  itg2addnclem3  26165  itg2addnc  26166  itg2gt0cn  26167  areacirclem2  26189  areacirc  26195  isbnd3  26391  cntotbnd  26403  rrnequiv  26442  irrapxlem3  26785  pellexlem2  26791  pellfundglb  26846  monotuz  26902  monotoddzzfi  26903  acongrep  26943  stoweidlem1  27625  stoweidlem3  27627  stoweidlem7  27631  stoweidlem24  27648  stoweidlem26  27650  stoweidlem42  27666  wallispilem5  27693  stirlinglem1  27698  stirlinglem6  27703  stirlinglem7  27704  stirlinglem10  27707  stirlinglem12  27709  stirlinglem13  27710  stirlingr  27714
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-13 1723  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-pow 4345  ax-pr 4371  ax-un 4668  ax-resscn 9011  ax-pre-lttri 9028
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-nel 2578  df-ral 2679  df-rex 2680  df-rab 2683  df-v 2926  df-sbc 3130  df-csb 3220  df-dif 3291  df-un 3293  df-in 3295  df-ss 3302  df-nul 3597  df-if 3708  df-pw 3769  df-sn 3788  df-pr 3789  df-op 3791  df-uni 3984  df-br 4181  df-opab 4235  df-mpt 4236  df-id 4466  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-rn 4856  df-res 4857  df-ima 4858  df-iota 5385  df-fun 5423  df-fn 5424  df-f 5425  df-f1 5426  df-fo 5427  df-f1o 5428  df-fv 5429  df-er 6872  df-en 7077  df-dom 7078  df-sdom 7079  df-pnf 9086  df-mnf 9087  df-xr 9088  df-ltxr 9089  df-le 9090
  Copyright terms: Public domain W3C validator