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

Theorem ltled 9623
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 9564 . . 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 1758   class class class wbr 4390   RRcr 9382    < clt 9519    <_ cle 9520
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-sep 4511  ax-nul 4519  ax-pow 4568  ax-pr 4629  ax-un 6472  ax-resscn 9440  ax-pre-lttri 9457
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-mo 2265  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-nel 2647  df-ral 2800  df-rex 2801  df-rab 2804  df-v 3070  df-sbc 3285  df-csb 3387  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-nul 3736  df-if 3890  df-pw 3960  df-sn 3976  df-pr 3978  df-op 3982  df-uni 4190  df-br 4391  df-opab 4449  df-mpt 4450  df-id 4734  df-xp 4944  df-rel 4945  df-cnv 4946  df-co 4947  df-dm 4948  df-rn 4949  df-res 4950  df-ima 4951  df-iota 5479  df-fun 5518  df-fn 5519  df-f 5520  df-f1 5521  df-fo 5522  df-f1o 5523  df-fv 5524  df-er 7201  df-en 7411  df-dom 7412  df-sdom 7413  df-pnf 9521  df-mnf 9522  df-xr 9523  df-ltxr 9524  df-le 9525
This theorem is referenced by:  ltnsymd  9624  mulge0  9958  msqge0  9962  addgt0d  10015  lt2addd  10062  lt2msq1  10316  uzwo3  11049  fznatpl1  11611  modaddmodup  11863  expmulnbnd  12097  fzsdom2  12291  repswcshw  12548  isercolllem1  13244  caucvgrlem  13252  climcnds  13416  geomulcvg  13438  mertenslem1  13446  ruclem2  13616  ruclem12  13625  bitsfzo  13733  bitsmod  13734  4sqlem7  14107  vdwlem1  14144  met1stc  20212  cfilucfilOLD  20260  cfilucfil  20261  nlmvscnlem2  20382  icccmplem2  20516  reconnlem2  20520  xrhmeo  20634  cnheibor  20643  nmoleub2lem3  20786  ipcnlem2  20872  minveclem3b  21031  ivthlem1  21051  ivthlem2  21052  ivth2  21055  ivthle  21056  ivthle2  21057  ovollb2lem  21087  ovolicc2lem4  21119  ovolicc2lem5  21120  ioombl1lem4  21158  uniioombllem4  21182  uniioombllem5  21183  opnmbllem  21197  ismbf3d  21248  mbfi1fseqlem6  21314  itg2gt0  21354  dveflem  21567  dvferm1lem  21572  dvferm2lem  21574  rollelem  21577  rolle  21578  cmvth  21579  mvth  21580  c1liplem1  21584  dvgt0lem1  21590  dvivthlem1  21596  lhop1lem  21601  lhop1  21602  dvcnvrelem1  21605  dvcnvrelem2  21606  dvcvx  21608  dgradd2  21851  aaliou3lem8  21927  aaliou3lem7  21931  ulmdvlem1  21981  itgulm  21989  radcnvlt1  21999  radcnvle  22001  abelthlem7  22019  efcvx  22030  coseq0negpitopi  22081  tangtx  22083  tanabsge  22084  tanord  22110  abslogimle  22141  divlogrlim  22196  logno1  22197  logcnlem3  22205  logcnlem4  22206  logtayl  22221  logccv  22224  cxple  22256  chordthmlem4  22346  asinsin  22403  atanlogaddlem  22424  atantan  22434  cxp2limlem  22485  logdifbnd  22503  emcllem4  22508  harmonicbnd4  22520  ftalem1  22526  ftalem2  22527  ftalem3  22528  basellem5  22538  basellem8  22541  chpchtsum  22674  bposlem1  22739  lgseisenlem1  22804  lgsquadlem1  22809  lgsquadlem2  22810  lgsquadlem3  22811  chebbnd1lem2  22835  chebbnd1lem3  22836  chtppilimlem1  22838  chto1ub  22841  chpo1ubb  22846  vmadivsumb  22848  dchrisumlem3  22856  mulog2sumlem1  22899  vmalogdivsum2  22903  vmalogdivsum  22904  2vmadivsumlem  22905  selbergb  22914  selberg2b  22917  chpdifbndlem1  22918  selberg3lem2  22923  selberg3  22924  selberg4lem1  22925  selberg4  22926  pntrsumbnd  22931  selberg3r  22934  selberg4r  22935  selberg34r  22936  pntrlog2bndlem1  22942  pntrlog2bndlem2  22943  pntrlog2bndlem3  22944  pntrlog2bndlem4  22945  pntrlog2bndlem5  22946  pntrlog2bndlem6a  22947  pntrlog2bndlem6  22948  pntrlog2bnd  22949  pntpbnd1a  22950  pntpbnd1  22951  pntpbnd2  22952  pntibndlem2  22956  pntlemb  22962  pntlemq  22966  pntlemr  22967  pntlemj  22968  pntlemf  22970  pntlemp  22975  ostth2lem2  22999  axpaschlem  23321  axlowdimlem16  23338  smcnlem  24227  bcm1n  26213  dya2icoseg  26826  eulerpartlemgc  26879  dstfrvunirn  26991  ballotlemfc0  27009  ballotlemfcc  27010  ballotlemimin  27022  ballotlemsgt1  27027  ballotlemfrcn0  27046  sgnmul  27059  lgamucov  27158  subfacval3  27211  erdszelem8  27220  cvmliftlem6  27313  cvmliftlem7  27314  cvmliftlem8  27315  cvmliftlem9  27316  cvmliftlem10  27317  sinccvglem  27451  lxflflp1  28559  opnmbllem0  28565  itg2addnclem  28581  itg2addnclem3  28583  itg2addnc  28584  itg2gt0cn  28585  areacirclem1  28622  areacirc  28627  isbnd3  28821  cntotbnd  28833  rrnequiv  28872  irrapxlem3  29303  pellexlem2  29309  pellfundglb  29364  monotuz  29420  monotoddzzfi  29421  acongrep  29461  stoweidlem1  29934  stoweidlem3  29936  stoweidlem7  29940  stoweidlem24  29957  stoweidlem26  29959  stoweidlem42  29975  wallispilem5  30002  stirlinglem1  30007  stirlinglem6  30012  stirlinglem7  30013  stirlinglem10  30016  stirlinglem12  30018  stirlinglem13  30019  stirlingr  30023
  Copyright terms: Public domain W3C validator