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

Theorem ltled 9772
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 9711 . . 3  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  <  B  ->  A  <_  B )
)
52, 3, 4syl2anc 665 . 2  |-  ( ph  ->  ( A  <  B  ->  A  <_  B )
)
61, 5mpd 15 1  |-  ( ph  ->  A  <_  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1867   class class class wbr 4417   RRcr 9527    < clt 9664    <_ cle 9665
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-8 1869  ax-9 1871  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398  ax-sep 4539  ax-nul 4547  ax-pow 4594  ax-pr 4652  ax-un 6588  ax-resscn 9585  ax-pre-lttri 9602
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2267  df-mo 2268  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-ne 2618  df-nel 2619  df-ral 2778  df-rex 2779  df-rab 2782  df-v 3080  df-sbc 3297  df-csb 3393  df-dif 3436  df-un 3438  df-in 3440  df-ss 3447  df-nul 3759  df-if 3907  df-pw 3978  df-sn 3994  df-pr 3996  df-op 4000  df-uni 4214  df-br 4418  df-opab 4476  df-mpt 4477  df-id 4760  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 5556  df-fun 5594  df-fn 5595  df-f 5596  df-f1 5597  df-fo 5598  df-f1o 5599  df-fv 5600  df-er 7362  df-en 7569  df-dom 7570  df-sdom 7571  df-pnf 9666  df-mnf 9667  df-xr 9668  df-ltxr 9669  df-le 9670
This theorem is referenced by:  ltnsymd  9773  mulge0  10121  msqge0  10124  addgt0d  10177  lt2addd  10225  lt2msq1  10479  uzwo3  11248  fznatpl1  11837  flflp1  12029  modaddmodup  12139  expmulnbnd  12390  fzsdom2  12584  repswcshw  12885  isercolllem1  13695  caucvgrlem  13703  caucvgrlemOLD  13704  climcnds  13876  geomulcvg  13899  mertenslem1  13907  ruclem2  14251  ruclem12  14260  bitsfzo  14372  bitsmod  14373  lcmgcdlem  14531  4sqlem7  14840  vdwlem1  14883  met1stc  21460  cfilucfil  21498  nlmvscnlem2  21612  icccmplem2  21745  reconnlem2  21749  xrhmeo  21863  cnheibor  21872  nmoleub2lem3  22015  ipcnlem2  22101  minveclem3b  22256  ivthlem1  22276  ivthlem2  22277  ivth2  22280  ivthle  22281  ivthle2  22282  ovollb2lem  22315  ovolicc2lem4OLD  22347  ovolicc2lem4  22348  ovolicc2lem5  22349  ioombl1lem4  22388  uniioombllem4  22418  uniioombllem5  22419  opnmbllem  22433  ismbf3d  22484  mbfi1fseqlem6  22552  itg2gt0  22592  dveflem  22805  dvferm1lem  22810  dvferm2lem  22812  rollelem  22815  rolle  22816  cmvth  22817  mvth  22818  c1liplem1  22822  dvgt0lem1  22828  dvivthlem1  22834  lhop1lem  22839  lhop1  22840  dvcnvrelem1  22843  dvcnvrelem2  22844  dvcvx  22846  dgradd2  23087  aaliou3lem8  23163  aaliou3lem7  23167  ulmdvlem1  23217  itgulm  23225  radcnvlt1  23235  radcnvle  23237  abelthlem7  23255  efcvx  23266  coseq0negpitopi  23320  tangtx  23322  tanabsge  23323  tanord  23349  abslogimle  23385  divlogrlim  23442  logno1  23443  logcnlem3  23451  logcnlem4  23452  logtayl  23467  logccv  23470  cxple  23502  chordthmlem4  23623  asinsin  23680  atanlogaddlem  23701  atantan  23711  cxp2limlem  23763  logdifbnd  23781  emcllem4  23786  harmonicbnd4  23798  lgamucov  23825  ftalem1  23859  ftalem2  23860  ftalem3  23861  basellem5  23871  basellem8  23874  chpchtsum  24007  bposlem1  24072  lgseisenlem1  24137  lgsquadlem1  24142  lgsquadlem2  24143  lgsquadlem3  24144  chebbnd1lem2  24168  chebbnd1lem3  24169  chtppilimlem1  24171  chto1ub  24174  chpo1ubb  24179  vmadivsumb  24181  dchrisumlem3  24189  mulog2sumlem1  24232  vmalogdivsum2  24236  vmalogdivsum  24237  2vmadivsumlem  24238  selbergb  24247  selberg2b  24250  chpdifbndlem1  24251  selberg3lem2  24256  selberg3  24257  selberg4lem1  24258  selberg4  24259  pntrsumbnd  24264  selberg3r  24267  selberg4r  24268  selberg34r  24269  pntrlog2bndlem1  24275  pntrlog2bndlem2  24276  pntrlog2bndlem3  24277  pntrlog2bndlem4  24278  pntrlog2bndlem5  24279  pntrlog2bndlem6a  24280  pntrlog2bndlem6  24281  pntrlog2bnd  24282  pntpbnd1a  24283  pntpbnd1  24284  pntpbnd2  24285  pntibndlem2  24289  pntlemb  24295  pntlemq  24299  pntlemr  24300  pntlemj  24301  pntlemf  24303  pntlemp  24308  ostth2lem2  24332  axpaschlem  24813  axlowdimlem16  24830  smcnlem  26175  bcm1n  28204  smatrcl  28458  fiunelros  28832  dya2icoseg  28935  eulerpartlemgc  29018  dstfrvunirn  29130  ballotlemfc0  29148  ballotlemfcc  29149  ballotlemimin  29161  ballotlemsgt1  29166  ballotlemfrcn0  29185  sgnmul  29198  subfacval3  29697  erdszelem8  29706  cvmliftlem6  29798  cvmliftlem7  29799  cvmliftlem8  29800  cvmliftlem9  29801  cvmliftlem10  29802  sinccvglem  30101  poimirlem7  31651  poimirlem15  31659  opnmbllem0  31680  itg2addnclem  31697  itg2addnclem3  31699  itg2addnc  31700  itg2gt0cn  31701  areacirclem1  31736  areacirc  31741  isbnd3  31820  cntotbnd  31832  rrnequiv  31871  irrapxlem3  35378  pellexlem2  35384  pellfundglb  35443  monotuz  35499  monotoddzzfi  35500  acongrep  35540  isprm7  36301  cvgdvgrat  36303  hashnzfz2  36311  hashnzfzclim  36312  binomcxplemnotnn0  36346  monoords  37127  limciccioolb  37277  limcicciooub  37293  lptre2pt  37296  icccncfext  37341  cncfiooicclem1  37347  dvdivbd  37371  dvbdfbdioolem1  37376  dvbdfbdioolem2  37377  ioodvbdlimc1lem2  37380  ioodvbdlimc2lem  37382  dvnxpaek  37390  dvnmul  37391  volioc  37422  iblspltprt  37423  itgspltprt  37429  stoweidlem1  37434  stoweidlem3  37436  stoweidlem7  37440  stoweidlem24  37457  stoweidlem26  37459  stoweidlem42  37476  wallispilem5  37504  stirlinglem1  37509  stirlinglem6  37514  stirlinglem7  37515  stirlinglem10  37518  stirlinglem12  37520  stirlinglem13  37521  stirlingr  37525  dirkertrigeqlem1  37533  fourierdlem10  37552  fourierdlem11  37553  fourierdlem12  37554  fourierdlem14  37556  fourierdlem15  37557  fourierdlem17  37559  fourierdlem19  37561  fourierdlem30  37572  fourierdlem37  37579  fourierdlem40  37582  fourierdlem41  37583  fourierdlem42  37584  fourierdlem47  37589  fourierdlem48  37590  fourierdlem49  37591  fourierdlem50  37592  fourierdlem51  37593  fourierdlem54  37596  fourierdlem63  37605  fourierdlem64  37606  fourierdlem65  37607  fourierdlem68  37610  fourierdlem73  37615  fourierdlem74  37616  fourierdlem76  37618  fourierdlem77  37619  fourierdlem78  37620  fourierdlem79  37621  fourierdlem81  37623  fourierdlem82  37624  fourierdlem83  37625  fourierdlem92  37634  fourierdlem93  37635  fourierdlem102  37644  fourierdlem103  37645  fourierdlem104  37646  fourierdlem107  37649  fourierdlem111  37653  fourierdlem114  37656  sqwvfoura  37664  sqwvfourb  37665  fouriersw  37667  etransclem19  37689  etransclem23  37693  etransclem35  37705  etransclem41  37711  iundjiun  37811  carageniuncllem2  37856  caratheodorylem1  37860  expnegico01  39088
  Copyright terms: Public domain W3C validator