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

Theorem ltled 9722
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 9662 . . 3  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  <  B  ->  A  <_  B )
)
52, 3, 4syl2anc 659 . 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 1823   class class class wbr 4439   RRcr 9480    < clt 9617    <_ cle 9618
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-8 1825  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pow 4615  ax-pr 4676  ax-un 6565  ax-resscn 9538  ax-pre-lttri 9555
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-nel 2652  df-ral 2809  df-rex 2810  df-rab 2813  df-v 3108  df-sbc 3325  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-if 3930  df-pw 4001  df-sn 4017  df-pr 4019  df-op 4023  df-uni 4236  df-br 4440  df-opab 4498  df-mpt 4499  df-id 4784  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-rn 4999  df-res 5000  df-ima 5001  df-iota 5534  df-fun 5572  df-fn 5573  df-f 5574  df-f1 5575  df-fo 5576  df-f1o 5577  df-fv 5578  df-er 7303  df-en 7510  df-dom 7511  df-sdom 7512  df-pnf 9619  df-mnf 9620  df-xr 9621  df-ltxr 9622  df-le 9623
This theorem is referenced by:  ltnsymd  9723  mulge0  10066  msqge0  10070  addgt0d  10123  lt2addd  10170  lt2msq1  10423  uzwo3  11178  fznatpl1  11738  flflp1  11925  modaddmodup  12032  expmulnbnd  12280  fzsdom2  12470  repswcshw  12771  isercolllem1  13569  caucvgrlem  13577  climcnds  13745  geomulcvg  13767  mertenslem1  13775  ruclem2  14049  ruclem12  14058  bitsfzo  14169  bitsmod  14170  4sqlem7  14546  vdwlem1  14583  met1stc  21190  cfilucfilOLD  21238  cfilucfil  21239  nlmvscnlem2  21360  icccmplem2  21494  reconnlem2  21498  xrhmeo  21612  cnheibor  21621  nmoleub2lem3  21764  ipcnlem2  21850  minveclem3b  22009  ivthlem1  22029  ivthlem2  22030  ivth2  22033  ivthle  22034  ivthle2  22035  ovollb2lem  22065  ovolicc2lem4  22097  ovolicc2lem5  22098  ioombl1lem4  22137  uniioombllem4  22161  uniioombllem5  22162  opnmbllem  22176  ismbf3d  22227  mbfi1fseqlem6  22293  itg2gt0  22333  dveflem  22546  dvferm1lem  22551  dvferm2lem  22553  rollelem  22556  rolle  22557  cmvth  22558  mvth  22559  c1liplem1  22563  dvgt0lem1  22569  dvivthlem1  22575  lhop1lem  22580  lhop1  22581  dvcnvrelem1  22584  dvcnvrelem2  22585  dvcvx  22587  dgradd2  22831  aaliou3lem8  22907  aaliou3lem7  22911  ulmdvlem1  22961  itgulm  22969  radcnvlt1  22979  radcnvle  22981  abelthlem7  22999  efcvx  23010  coseq0negpitopi  23062  tangtx  23064  tanabsge  23065  tanord  23091  abslogimle  23127  divlogrlim  23184  logno1  23185  logcnlem3  23193  logcnlem4  23194  logtayl  23209  logccv  23212  cxple  23244  chordthmlem4  23363  asinsin  23420  atanlogaddlem  23441  atantan  23451  cxp2limlem  23503  logdifbnd  23521  emcllem4  23526  harmonicbnd4  23538  ftalem1  23544  ftalem2  23545  ftalem3  23546  basellem5  23556  basellem8  23559  chpchtsum  23692  bposlem1  23757  lgseisenlem1  23822  lgsquadlem1  23827  lgsquadlem2  23828  lgsquadlem3  23829  chebbnd1lem2  23853  chebbnd1lem3  23854  chtppilimlem1  23856  chto1ub  23859  chpo1ubb  23864  vmadivsumb  23866  dchrisumlem3  23874  mulog2sumlem1  23917  vmalogdivsum2  23921  vmalogdivsum  23922  2vmadivsumlem  23923  selbergb  23932  selberg2b  23935  chpdifbndlem1  23936  selberg3lem2  23941  selberg3  23942  selberg4lem1  23943  selberg4  23944  pntrsumbnd  23949  selberg3r  23952  selberg4r  23953  selberg34r  23954  pntrlog2bndlem1  23960  pntrlog2bndlem2  23961  pntrlog2bndlem3  23962  pntrlog2bndlem4  23963  pntrlog2bndlem5  23964  pntrlog2bndlem6a  23965  pntrlog2bndlem6  23966  pntrlog2bnd  23967  pntpbnd1a  23968  pntpbnd1  23969  pntpbnd2  23970  pntibndlem2  23974  pntlemb  23980  pntlemq  23984  pntlemr  23985  pntlemj  23986  pntlemf  23988  pntlemp  23993  ostth2lem2  24017  axpaschlem  24445  axlowdimlem16  24462  smcnlem  25805  bcm1n  27834  dya2icoseg  28485  eulerpartlemgc  28565  dstfrvunirn  28677  ballotlemfc0  28695  ballotlemfcc  28696  ballotlemimin  28708  ballotlemsgt1  28713  ballotlemfrcn0  28732  sgnmul  28745  lgamucov  28844  subfacval3  28897  erdszelem8  28906  cvmliftlem6  28999  cvmliftlem7  29000  cvmliftlem8  29001  cvmliftlem9  29002  cvmliftlem10  29003  sinccvglem  29302  opnmbllem0  30290  itg2addnclem  30306  itg2addnclem3  30308  itg2addnc  30309  itg2gt0cn  30310  areacirclem1  30347  areacirc  30352  isbnd3  30520  cntotbnd  30532  rrnequiv  30571  irrapxlem3  30999  pellexlem2  31005  pellfundglb  31060  monotuz  31116  monotoddzzfi  31117  acongrep  31157  isprm7  31433  cvgdvgrat  31435  lcmgcdlem  31453  hashnzfz2  31467  hashnzfzclim  31468  binomcxplemnotnn0  31502  monoords  31735  limciccioolb  31866  limcicciooub  31882  lptre2pt  31885  icccncfext  31929  cncfiooicclem1  31935  dvdivbd  31959  dvbdfbdioolem1  31964  dvbdfbdioolem2  31965  ioodvbdlimc1lem2  31968  ioodvbdlimc2lem  31970  dvnxpaek  31978  dvnmul  31979  volioc  32010  iblspltprt  32011  itgspltprt  32017  stoweidlem1  32022  stoweidlem3  32024  stoweidlem7  32028  stoweidlem24  32045  stoweidlem26  32047  stoweidlem42  32063  wallispilem5  32090  stirlinglem1  32095  stirlinglem6  32100  stirlinglem7  32101  stirlinglem10  32104  stirlinglem12  32106  stirlinglem13  32107  stirlingr  32111  dirkertrigeqlem1  32119  fourierdlem10  32138  fourierdlem11  32139  fourierdlem12  32140  fourierdlem14  32142  fourierdlem15  32143  fourierdlem17  32145  fourierdlem19  32147  fourierdlem30  32158  fourierdlem37  32165  fourierdlem40  32168  fourierdlem41  32169  fourierdlem42  32170  fourierdlem47  32175  fourierdlem48  32176  fourierdlem49  32177  fourierdlem50  32178  fourierdlem51  32179  fourierdlem54  32182  fourierdlem63  32191  fourierdlem64  32192  fourierdlem65  32193  fourierdlem68  32196  fourierdlem73  32201  fourierdlem74  32202  fourierdlem76  32204  fourierdlem77  32205  fourierdlem78  32206  fourierdlem79  32207  fourierdlem81  32209  fourierdlem82  32210  fourierdlem83  32211  fourierdlem92  32220  fourierdlem93  32221  fourierdlem102  32230  fourierdlem103  32231  fourierdlem104  32232  fourierdlem107  32235  fourierdlem111  32239  fourierdlem114  32242  sqwvfoura  32250  sqwvfourb  32251  fouriersw  32253  etransclem19  32275  etransclem23  32279  etransclem35  32291  etransclem41  32297  expnegico01  33377
  Copyright terms: Public domain W3C validator