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

Theorem ltled 9057
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 9000 . . 3  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  <  B  ->  A  <_  B )
)
52, 3, 4syl2anc 642 . 2  |-  ( ph  ->  ( A  <  B  ->  A  <_  B )
)
61, 5mpd 14 1  |-  ( ph  ->  A  <_  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1710   class class class wbr 4104   RRcr 8826    < clt 8957    <_ cle 8958
This theorem is referenced by:  ltnsymd  9058  mulge0  9381  msqge0  9385  addgt0d  9437  lt2addd  9484  lt2msq1  9729  uzwo3  10403  expmulnbnd  11326  fzsdom2  11478  isercolllem1  12234  caucvgrlem  12242  climcnds  12407  geomulcvg  12429  mertenslem1  12437  ruclem2  12607  ruclem12  12616  bitsfzo  12723  bitsmod  12724  4sqlem7  13088  vdwlem1  13125  met1stc  18169  nlmvscnlem2  18298  icccmplem2  18431  reconnlem2  18435  xrhmeo  18548  cnheibor  18557  nmoleub2lem3  18700  ipcnlem2  18775  minveclem3b  18896  ivthlem1  18915  ivthlem2  18916  ivth2  18919  ivthle  18920  ivthle2  18921  ovollb2lem  18951  ovolicc2lem4  18983  ovolicc2lem5  18984  ioombl1lem4  19022  uniioombllem4  19045  uniioombllem5  19046  opnmbllem  19060  ismbf3d  19113  mbfi1fseqlem6  19179  itg2gt0  19219  dveflem  19430  dvferm1lem  19435  dvferm2lem  19437  rollelem  19440  rolle  19441  cmvth  19442  mvth  19443  c1liplem1  19447  dvgt0lem1  19453  dvivthlem1  19459  lhop1lem  19464  lhop1  19465  dvcnvrelem1  19468  dvcnvrelem2  19469  dvcvx  19471  dgradd2  19753  aaliou3lem8  19829  aaliou3lem7  19833  ulmdvlem1  19883  itgulm  19891  radcnvlt1  19901  radcnvle  19903  abelthlem7  19921  efcvx  19932  coseq0negpitopi  19978  tangtx  19980  tanabsge  19981  tanord  20007  abslogimle  20038  divlogrlim  20093  logno1  20094  logcnlem3  20102  logcnlem4  20103  logtayl  20118  logccv  20121  cxple  20153  chordthmlem4  20243  asinsin  20299  atanlogaddlem  20320  atantan  20330  cxp2limlem  20381  logdifbnd  20399  emcllem4  20404  harmonicbnd4  20416  ftalem1  20422  ftalem2  20423  ftalem3  20424  basellem5  20434  basellem8  20437  chpchtsum  20570  bposlem1  20635  lgseisenlem1  20700  lgsquadlem1  20705  lgsquadlem2  20706  lgsquadlem3  20707  chebbnd1lem2  20731  chebbnd1lem3  20732  chtppilimlem1  20734  chto1ub  20737  chpo1ubb  20742  vmadivsumb  20744  dchrisumlem3  20752  mulog2sumlem1  20795  vmalogdivsum2  20799  vmalogdivsum  20800  2vmadivsumlem  20801  selbergb  20810  selberg2b  20813  chpdifbndlem1  20814  selberg3lem2  20819  selberg3  20820  selberg4lem1  20821  selberg4  20822  pntrsumbnd  20827  selberg3r  20830  selberg4r  20831  selberg34r  20832  pntrlog2bndlem1  20838  pntrlog2bndlem2  20839  pntrlog2bndlem3  20840  pntrlog2bndlem4  20841  pntrlog2bndlem5  20842  pntrlog2bndlem6a  20843  pntrlog2bndlem6  20844  pntrlog2bnd  20845  pntpbnd1a  20846  pntpbnd1  20847  pntpbnd2  20848  pntibndlem2  20852  pntlemb  20858  pntlemq  20862  pntlemr  20863  pntlemj  20864  pntlemf  20866  pntlemp  20871  ostth2lem2  20895  smcnlem  21384  bcm1n  23353  cfilucfil  23603  dya2icoseg  23891  dstfrvunirn  23981  ballotlemfc0  23999  ballotlemfcc  24000  ballotlemimin  24012  ballotlemfrcn0  24036  lgamucov  24071  subfacval3  24124  erdszelem8  24133  cvmliftlem6  24225  cvmliftlem7  24226  cvmliftlem8  24227  cvmliftlem9  24228  cvmliftlem10  24229  sinccvglem  24409  fznatpl1  24499  axpaschlem  25127  axlowdimlem16  25144  lxflflp1  25487  itg2addnclem  25492  itg2gt0cn  25495  areacirclem2  25517  areacirc  25523  isbnd3  25831  cntotbnd  25843  rrnequiv  25882  irrapxlem3  26232  pellexlem2  26238  pellfundglb  26293  monotuz  26349  monotoddzzfi  26350  acongrep  26390  stirlinglem1  27146  stirlinglem6  27151  stirlinglem7  27152  stirlinglem10  27155  stirlinglem12  27157  stirlinglem13  27158  stirlingr  27162
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339  ax-sep 4222  ax-nul 4230  ax-pow 4269  ax-pr 4295  ax-un 4594  ax-resscn 8884  ax-pre-lttri 8901
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2213  df-mo 2214  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ne 2523  df-nel 2524  df-ral 2624  df-rex 2625  df-rab 2628  df-v 2866  df-sbc 3068  df-csb 3158  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-nul 3532  df-if 3642  df-pw 3703  df-sn 3722  df-pr 3723  df-op 3725  df-uni 3909  df-br 4105  df-opab 4159  df-mpt 4160  df-id 4391  df-xp 4777  df-rel 4778  df-cnv 4779  df-co 4780  df-dm 4781  df-rn 4782  df-res 4783  df-ima 4784  df-iota 5301  df-fun 5339  df-fn 5340  df-f 5341  df-f1 5342  df-fo 5343  df-f1o 5344  df-fv 5345  df-er 6747  df-en 6952  df-dom 6953  df-sdom 6954  df-pnf 8959  df-mnf 8960  df-xr 8961  df-ltxr 8962  df-le 8963
  Copyright terms: Public domain W3C validator