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

Theorem ltled 9226
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 9168 . . 3  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  <  B  ->  A  <_  B )
)
52, 3, 4syl2anc 644 . 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 1726   class class class wbr 4215   RRcr 8994    < clt 9125    <_ cle 9126
This theorem is referenced by:  ltnsymd  9227  mulge0  9550  msqge0  9554  addgt0d  9606  lt2addd  9653  lt2msq1  9898  uzwo3  10574  expmulnbnd  11516  fzsdom2  11698  isercolllem1  12463  caucvgrlem  12471  climcnds  12636  geomulcvg  12658  mertenslem1  12666  ruclem2  12836  ruclem12  12845  bitsfzo  12952  bitsmod  12953  4sqlem7  13317  vdwlem1  13354  met1stc  18556  cfilucfilOLD  18604  cfilucfil  18605  nlmvscnlem2  18726  icccmplem2  18859  reconnlem2  18863  xrhmeo  18976  cnheibor  18985  nmoleub2lem3  19128  ipcnlem2  19203  minveclem3b  19334  ivthlem1  19353  ivthlem2  19354  ivth2  19357  ivthle  19358  ivthle2  19359  ovollb2lem  19389  ovolicc2lem4  19421  ovolicc2lem5  19422  ioombl1lem4  19460  uniioombllem4  19483  uniioombllem5  19484  opnmbllem  19498  ismbf3d  19549  mbfi1fseqlem6  19615  itg2gt0  19655  dveflem  19868  dvferm1lem  19873  dvferm2lem  19875  rollelem  19878  rolle  19879  cmvth  19880  mvth  19881  c1liplem1  19885  dvgt0lem1  19891  dvivthlem1  19897  lhop1lem  19902  lhop1  19903  dvcnvrelem1  19906  dvcnvrelem2  19907  dvcvx  19909  dgradd2  20191  aaliou3lem8  20267  aaliou3lem7  20271  ulmdvlem1  20321  itgulm  20329  radcnvlt1  20339  radcnvle  20341  abelthlem7  20359  efcvx  20370  coseq0negpitopi  20416  tangtx  20418  tanabsge  20419  tanord  20445  abslogimle  20476  divlogrlim  20531  logno1  20532  logcnlem3  20540  logcnlem4  20541  logtayl  20556  logccv  20559  cxple  20591  chordthmlem4  20681  asinsin  20737  atanlogaddlem  20758  atantan  20768  cxp2limlem  20819  logdifbnd  20837  emcllem4  20842  harmonicbnd4  20854  ftalem1  20860  ftalem2  20861  ftalem3  20862  basellem5  20872  basellem8  20875  chpchtsum  21008  bposlem1  21073  lgseisenlem1  21138  lgsquadlem1  21143  lgsquadlem2  21144  lgsquadlem3  21145  chebbnd1lem2  21169  chebbnd1lem3  21170  chtppilimlem1  21172  chto1ub  21175  chpo1ubb  21180  vmadivsumb  21182  dchrisumlem3  21190  mulog2sumlem1  21233  vmalogdivsum2  21237  vmalogdivsum  21238  2vmadivsumlem  21239  selbergb  21248  selberg2b  21251  chpdifbndlem1  21252  selberg3lem2  21257  selberg3  21258  selberg4lem1  21259  selberg4  21260  pntrsumbnd  21265  selberg3r  21268  selberg4r  21269  selberg34r  21270  pntrlog2bndlem1  21276  pntrlog2bndlem2  21277  pntrlog2bndlem3  21278  pntrlog2bndlem4  21279  pntrlog2bndlem5  21280  pntrlog2bndlem6a  21281  pntrlog2bndlem6  21282  pntrlog2bnd  21283  pntpbnd1a  21284  pntpbnd1  21285  pntpbnd2  21286  pntibndlem2  21290  pntlemb  21296  pntlemq  21300  pntlemr  21301  pntlemj  21302  pntlemf  21304  pntlemp  21309  ostth2lem2  21333  smcnlem  22198  bcm1n  24156  dya2icoseg  24632  dstfrvunirn  24737  ballotlemfc0  24755  ballotlemfcc  24756  ballotlemimin  24768  ballotlemsgt1  24773  ballotlemfrcn0  24792  lgamucov  24827  subfacval3  24880  erdszelem8  24889  cvmliftlem6  24982  cvmliftlem7  24983  cvmliftlem8  24984  cvmliftlem9  24985  cvmliftlem10  24986  sinccvglem  25114  fznatpl1  25203  axpaschlem  25884  axlowdimlem16  25901  lxflflp1  26249  opnmbllem0  26254  itg2addnclem  26270  itg2addnclem3  26272  itg2addnc  26273  itg2gt0cn  26274  areacirclem1  26306  areacirc  26311  isbnd3  26507  cntotbnd  26519  rrnequiv  26558  irrapxlem3  26901  pellexlem2  26907  pellfundglb  26962  monotuz  27018  monotoddzzfi  27019  acongrep  27059  stoweidlem1  27740  stoweidlem3  27742  stoweidlem7  27746  stoweidlem24  27763  stoweidlem26  27765  stoweidlem42  27781  wallispilem5  27808  stirlinglem1  27813  stirlinglem6  27818  stirlinglem7  27819  stirlinglem10  27822  stirlinglem12  27824  stirlinglem13  27825  stirlingr  27829
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-sep 4333  ax-nul 4341  ax-pow 4380  ax-pr 4406  ax-un 4704  ax-resscn 9052  ax-pre-lttri 9069
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-nel 2604  df-ral 2712  df-rex 2713  df-rab 2716  df-v 2960  df-sbc 3164  df-csb 3254  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-pw 3803  df-sn 3822  df-pr 3823  df-op 3825  df-uni 4018  df-br 4216  df-opab 4270  df-mpt 4271  df-id 4501  df-xp 4887  df-rel 4888  df-cnv 4889  df-co 4890  df-dm 4891  df-rn 4892  df-res 4893  df-ima 4894  df-iota 5421  df-fun 5459  df-fn 5460  df-f 5461  df-f1 5462  df-fo 5463  df-f1o 5464  df-fv 5465  df-er 6908  df-en 7113  df-dom 7114  df-sdom 7115  df-pnf 9127  df-mnf 9128  df-xr 9129  df-ltxr 9130  df-le 9131
  Copyright terms: Public domain W3C validator