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

Theorem ltled 9721
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 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 1762   class class class wbr 4440   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 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-8 1764  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-sep 4561  ax-nul 4569  ax-pow 4618  ax-pr 4679  ax-un 6567  ax-resscn 9538  ax-pre-lttri 9555
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-eu 2272  df-mo 2273  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-nel 2658  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3108  df-sbc 3325  df-csb 3429  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-pw 4005  df-sn 4021  df-pr 4023  df-op 4027  df-uni 4239  df-br 4441  df-opab 4499  df-mpt 4500  df-id 4788  df-xp 4998  df-rel 4999  df-cnv 5000  df-co 5001  df-dm 5002  df-rn 5003  df-res 5004  df-ima 5005  df-iota 5542  df-fun 5581  df-fn 5582  df-f 5583  df-f1 5584  df-fo 5585  df-f1o 5586  df-fv 5587  df-er 7301  df-en 7507  df-dom 7508  df-sdom 7509  df-pnf 9619  df-mnf 9620  df-xr 9621  df-ltxr 9622  df-le 9623
This theorem is referenced by:  ltnsymd  9722  mulge0  10059  msqge0  10063  addgt0d  10116  lt2addd  10163  lt2msq1  10417  uzwo3  11166  fznatpl1  11723  modaddmodup  12006  expmulnbnd  12253  fzsdom2  12438  repswcshw  12730  isercolllem1  13436  caucvgrlem  13444  climcnds  13615  geomulcvg  13637  mertenslem1  13645  ruclem2  13815  ruclem12  13824  bitsfzo  13933  bitsmod  13934  4sqlem7  14310  vdwlem1  14347  met1stc  20752  cfilucfilOLD  20800  cfilucfil  20801  nlmvscnlem2  20922  icccmplem2  21056  reconnlem2  21060  xrhmeo  21174  cnheibor  21183  nmoleub2lem3  21326  ipcnlem2  21412  minveclem3b  21571  ivthlem1  21591  ivthlem2  21592  ivth2  21595  ivthle  21596  ivthle2  21597  ovollb2lem  21627  ovolicc2lem4  21659  ovolicc2lem5  21660  ioombl1lem4  21699  uniioombllem4  21723  uniioombllem5  21724  opnmbllem  21738  ismbf3d  21789  mbfi1fseqlem6  21855  itg2gt0  21895  dveflem  22108  dvferm1lem  22113  dvferm2lem  22115  rollelem  22118  rolle  22119  cmvth  22120  mvth  22121  c1liplem1  22125  dvgt0lem1  22131  dvivthlem1  22137  lhop1lem  22142  lhop1  22143  dvcnvrelem1  22146  dvcnvrelem2  22147  dvcvx  22149  dgradd2  22392  aaliou3lem8  22468  aaliou3lem7  22472  ulmdvlem1  22522  itgulm  22530  radcnvlt1  22540  radcnvle  22542  abelthlem7  22560  efcvx  22571  coseq0negpitopi  22622  tangtx  22624  tanabsge  22625  tanord  22651  abslogimle  22682  divlogrlim  22737  logno1  22738  logcnlem3  22746  logcnlem4  22747  logtayl  22762  logccv  22765  cxple  22797  chordthmlem4  22887  asinsin  22944  atanlogaddlem  22965  atantan  22975  cxp2limlem  23026  logdifbnd  23044  emcllem4  23049  harmonicbnd4  23061  ftalem1  23067  ftalem2  23068  ftalem3  23069  basellem5  23079  basellem8  23082  chpchtsum  23215  bposlem1  23280  lgseisenlem1  23345  lgsquadlem1  23350  lgsquadlem2  23351  lgsquadlem3  23352  chebbnd1lem2  23376  chebbnd1lem3  23377  chtppilimlem1  23379  chto1ub  23382  chpo1ubb  23387  vmadivsumb  23389  dchrisumlem3  23397  mulog2sumlem1  23440  vmalogdivsum2  23444  vmalogdivsum  23445  2vmadivsumlem  23446  selbergb  23455  selberg2b  23458  chpdifbndlem1  23459  selberg3lem2  23464  selberg3  23465  selberg4lem1  23466  selberg4  23467  pntrsumbnd  23472  selberg3r  23475  selberg4r  23476  selberg34r  23477  pntrlog2bndlem1  23483  pntrlog2bndlem2  23484  pntrlog2bndlem3  23485  pntrlog2bndlem4  23486  pntrlog2bndlem5  23487  pntrlog2bndlem6a  23488  pntrlog2bndlem6  23489  pntrlog2bnd  23490  pntpbnd1a  23491  pntpbnd1  23492  pntpbnd2  23493  pntibndlem2  23497  pntlemb  23503  pntlemq  23507  pntlemr  23508  pntlemj  23509  pntlemf  23511  pntlemp  23516  ostth2lem2  23540  axpaschlem  23912  axlowdimlem16  23929  smcnlem  25133  bcm1n  27118  dya2icoseg  27738  eulerpartlemgc  27791  dstfrvunirn  27903  ballotlemfc0  27921  ballotlemfcc  27922  ballotlemimin  27934  ballotlemsgt1  27939  ballotlemfrcn0  27958  sgnmul  27971  lgamucov  28070  subfacval3  28123  erdszelem8  28132  cvmliftlem6  28225  cvmliftlem7  28226  cvmliftlem8  28227  cvmliftlem9  28228  cvmliftlem10  28229  sinccvglem  28363  lxflflp1  29472  opnmbllem0  29478  itg2addnclem  29494  itg2addnclem3  29496  itg2addnc  29497  itg2gt0cn  29498  areacirclem1  29535  areacirc  29540  isbnd3  29734  cntotbnd  29746  rrnequiv  29785  irrapxlem3  30215  pellexlem2  30221  pellfundglb  30276  monotuz  30332  monotoddzzfi  30333  acongrep  30373  monoords  30892  limciccioolb  30982  limcicciooub  30998  lptre2pt  31001  icccncfext  31045  dvdivbd  31072  dvbdfbdioolem1  31077  dvbdfbdioolem2  31078  ioodvbdlimc1lem2  31081  ioodvbdlimc2lem  31083  volioc  31109  iblspltprt  31110  itgspltprt  31116  stoweidlem1  31120  stoweidlem3  31122  stoweidlem7  31126  stoweidlem24  31143  stoweidlem26  31145  stoweidlem42  31161  wallispilem5  31188  stirlinglem1  31193  stirlinglem6  31198  stirlinglem7  31199  stirlinglem10  31202  stirlinglem12  31204  stirlinglem13  31205  stirlingr  31209  dirkertrigeqlem1  31217  fourierdlem10  31236  fourierdlem11  31237  fourierdlem12  31238  fourierdlem14  31240  fourierdlem15  31241  fourierdlem17  31243  fourierdlem19  31245  fourierdlem20  31246  fourierdlem25  31251  fourierdlem30  31256  fourierdlem37  31263  fourierdlem39  31265  fourierdlem40  31266  fourierdlem41  31267  fourierdlem42  31268  fourierdlem47  31273  fourierdlem48  31274  fourierdlem49  31275  fourierdlem50  31276  fourierdlem51  31277  fourierdlem54  31280  fourierdlem63  31289  fourierdlem64  31290  fourierdlem65  31291  fourierdlem68  31294  fourierdlem73  31299  fourierdlem74  31300  fourierdlem75  31301  fourierdlem76  31302  fourierdlem77  31303  fourierdlem78  31304  fourierdlem79  31305  fourierdlem81  31307  fourierdlem82  31308  fourierdlem83  31309  fourierdlem92  31318  fourierdlem93  31319  fourierdlem102  31328  fourierdlem103  31329  fourierdlem104  31330  fourierdlem107  31333  fourierdlem111  31337  fourierdlem114  31340  sqwvfoura  31348  sqwvfourb  31349  fouriersw  31351
  Copyright terms: Public domain W3C validator