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

Theorem ltled 9731
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 9671 . . 3  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  <  B  ->  A  <_  B )
)
52, 3, 4syl2anc 661 . 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 1802   class class class wbr 4433   RRcr 9489    < clt 9626    <_ cle 9627
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-8 1804  ax-9 1806  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-sep 4554  ax-nul 4562  ax-pow 4611  ax-pr 4672  ax-un 6573  ax-resscn 9547  ax-pre-lttri 9564
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-eu 2270  df-mo 2271  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-nel 2639  df-ral 2796  df-rex 2797  df-rab 2800  df-v 3095  df-sbc 3312  df-csb 3418  df-dif 3461  df-un 3463  df-in 3465  df-ss 3472  df-nul 3768  df-if 3923  df-pw 3995  df-sn 4011  df-pr 4013  df-op 4017  df-uni 4231  df-br 4434  df-opab 4492  df-mpt 4493  df-id 4781  df-xp 4991  df-rel 4992  df-cnv 4993  df-co 4994  df-dm 4995  df-rn 4996  df-res 4997  df-ima 4998  df-iota 5537  df-fun 5576  df-fn 5577  df-f 5578  df-f1 5579  df-fo 5580  df-f1o 5581  df-fv 5582  df-er 7309  df-en 7515  df-dom 7516  df-sdom 7517  df-pnf 9628  df-mnf 9629  df-xr 9630  df-ltxr 9631  df-le 9632
This theorem is referenced by:  ltnsymd  9732  mulge0  10071  msqge0  10075  addgt0d  10128  lt2addd  10175  lt2msq1  10429  uzwo3  11181  fznatpl1  11738  flflp1  11918  modaddmodup  12024  expmulnbnd  12272  fzsdom2  12460  repswcshw  12754  isercolllem1  13461  caucvgrlem  13469  climcnds  13637  geomulcvg  13659  mertenslem1  13667  ruclem2  13837  ruclem12  13846  bitsfzo  13957  bitsmod  13958  4sqlem7  14334  vdwlem1  14371  met1stc  20890  cfilucfilOLD  20938  cfilucfil  20939  nlmvscnlem2  21060  icccmplem2  21194  reconnlem2  21198  xrhmeo  21312  cnheibor  21321  nmoleub2lem3  21464  ipcnlem2  21550  minveclem3b  21709  ivthlem1  21729  ivthlem2  21730  ivth2  21733  ivthle  21734  ivthle2  21735  ovollb2lem  21765  ovolicc2lem4  21797  ovolicc2lem5  21798  ioombl1lem4  21837  uniioombllem4  21861  uniioombllem5  21862  opnmbllem  21876  ismbf3d  21927  mbfi1fseqlem6  21993  itg2gt0  22033  dveflem  22246  dvferm1lem  22251  dvferm2lem  22253  rollelem  22256  rolle  22257  cmvth  22258  mvth  22259  c1liplem1  22263  dvgt0lem1  22269  dvivthlem1  22275  lhop1lem  22280  lhop1  22281  dvcnvrelem1  22284  dvcnvrelem2  22285  dvcvx  22287  dgradd2  22530  aaliou3lem8  22606  aaliou3lem7  22610  ulmdvlem1  22660  itgulm  22668  radcnvlt1  22678  radcnvle  22680  abelthlem7  22698  efcvx  22709  coseq0negpitopi  22761  tangtx  22763  tanabsge  22764  tanord  22790  abslogimle  22826  divlogrlim  22881  logno1  22882  logcnlem3  22890  logcnlem4  22891  logtayl  22906  logccv  22909  cxple  22941  chordthmlem4  23031  asinsin  23088  atanlogaddlem  23109  atantan  23119  cxp2limlem  23170  logdifbnd  23188  emcllem4  23193  harmonicbnd4  23205  ftalem1  23211  ftalem2  23212  ftalem3  23213  basellem5  23223  basellem8  23226  chpchtsum  23359  bposlem1  23424  lgseisenlem1  23489  lgsquadlem1  23494  lgsquadlem2  23495  lgsquadlem3  23496  chebbnd1lem2  23520  chebbnd1lem3  23521  chtppilimlem1  23523  chto1ub  23526  chpo1ubb  23531  vmadivsumb  23533  dchrisumlem3  23541  mulog2sumlem1  23584  vmalogdivsum2  23588  vmalogdivsum  23589  2vmadivsumlem  23590  selbergb  23599  selberg2b  23602  chpdifbndlem1  23603  selberg3lem2  23608  selberg3  23609  selberg4lem1  23610  selberg4  23611  pntrsumbnd  23616  selberg3r  23619  selberg4r  23620  selberg34r  23621  pntrlog2bndlem1  23627  pntrlog2bndlem2  23628  pntrlog2bndlem3  23629  pntrlog2bndlem4  23630  pntrlog2bndlem5  23631  pntrlog2bndlem6a  23632  pntrlog2bndlem6  23633  pntrlog2bnd  23634  pntpbnd1a  23635  pntpbnd1  23636  pntpbnd2  23637  pntibndlem2  23641  pntlemb  23647  pntlemq  23651  pntlemr  23652  pntlemj  23653  pntlemf  23655  pntlemp  23660  ostth2lem2  23684  axpaschlem  24108  axlowdimlem16  24125  smcnlem  25472  bcm1n  27465  dya2icoseg  28114  eulerpartlemgc  28167  dstfrvunirn  28279  ballotlemfc0  28297  ballotlemfcc  28298  ballotlemimin  28310  ballotlemsgt1  28315  ballotlemfrcn0  28334  sgnmul  28347  lgamucov  28446  subfacval3  28499  erdszelem8  28508  cvmliftlem6  28601  cvmliftlem7  28602  cvmliftlem8  28603  cvmliftlem9  28604  cvmliftlem10  28605  sinccvglem  28904  opnmbllem0  30018  itg2addnclem  30034  itg2addnclem3  30036  itg2addnc  30037  itg2gt0cn  30038  areacirclem1  30075  areacirc  30080  isbnd3  30248  cntotbnd  30260  rrnequiv  30299  irrapxlem3  30728  pellexlem2  30734  pellfundglb  30789  monotuz  30845  monotoddzzfi  30846  acongrep  30886  isprm7  31161  cvgdvgrat  31163  lcmgcdlem  31181  hashnzfz2  31195  hashnzfzclim  31196  monoords  31441  limciccioolb  31531  limcicciooub  31547  lptre2pt  31550  icccncfext  31593  cncfiooicclem1  31599  dvdivbd  31620  dvbdfbdioolem1  31625  dvbdfbdioolem2  31626  ioodvbdlimc1lem2  31629  ioodvbdlimc2lem  31631  volioc  31657  iblspltprt  31658  itgspltprt  31664  stoweidlem1  31668  stoweidlem3  31670  stoweidlem7  31674  stoweidlem24  31691  stoweidlem26  31693  stoweidlem42  31709  wallispilem5  31736  stirlinglem1  31741  stirlinglem6  31746  stirlinglem7  31747  stirlinglem10  31750  stirlinglem12  31752  stirlinglem13  31753  stirlingr  31757  dirkertrigeqlem1  31765  fourierdlem10  31784  fourierdlem11  31785  fourierdlem12  31786  fourierdlem14  31788  fourierdlem15  31789  fourierdlem17  31791  fourierdlem19  31793  fourierdlem30  31804  fourierdlem37  31811  fourierdlem40  31814  fourierdlem41  31815  fourierdlem42  31816  fourierdlem47  31821  fourierdlem48  31822  fourierdlem49  31823  fourierdlem50  31824  fourierdlem51  31825  fourierdlem54  31828  fourierdlem63  31837  fourierdlem64  31838  fourierdlem65  31839  fourierdlem68  31842  fourierdlem73  31847  fourierdlem74  31848  fourierdlem76  31850  fourierdlem77  31851  fourierdlem78  31852  fourierdlem79  31853  fourierdlem81  31855  fourierdlem82  31856  fourierdlem83  31857  fourierdlem92  31866  fourierdlem93  31867  fourierdlem102  31876  fourierdlem103  31877  fourierdlem104  31878  fourierdlem107  31881  fourierdlem111  31885  fourierdlem114  31888  sqwvfoura  31896  sqwvfourb  31897  fouriersw  31899
  Copyright terms: Public domain W3C validator