Theorem ltled 11106

Description: 'Less than' implies 'less than or equal to'. (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
ltd.1	⊢ (𝜑 → 𝐴 ∈ ℝ)
ltd.2	⊢ (𝜑 → 𝐵 ∈ ℝ)
ltled.1	⊢ (𝜑 → 𝐴 < 𝐵)

Assertion

Ref	Expression
ltled	⊢ (𝜑 → 𝐴 ≤ 𝐵)

Proof of Theorem ltled

Step	Hyp	Ref	Expression
1		ltled.1	. 2 ⊢ (𝜑 → 𝐴 < 𝐵)
2		ltd.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ ℝ)
3		ltd.2	. . 3 ⊢ (𝜑 → 𝐵 ∈ ℝ)
4		ltle 11047	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 → 𝐴 ≤ 𝐵))
5	2, 3, 4	syl2anc 583	. 2 ⊢ (𝜑 → (𝐴 < 𝐵 → 𝐴 ≤ 𝐵))
6	1, 5	mpd 15	1 ⊢ (𝜑 → 𝐴 ≤ 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2109   class class class wbr 5078  ℝcr 10854   < clt 10993   ≤ cle 10994

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-10 2140  ax-11 2157  ax-12 2174  ax-ext 2710  ax-sep 5226  ax-nul 5233  ax-pow 5291  ax-pr 5355  ax-un 7579  ax-resscn 10912  ax-pre-lttri 10929

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-nf 1790  df-sb 2071  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3432  df-sbc 3720  df-csb 3837  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-nul 4262  df-if 4465  df-pw 4540  df-sn 4567  df-pr 4569  df-op 4573  df-uni 4845  df-br 5079  df-opab 5141  df-mpt 5162  df-id 5488  df-xp 5594  df-rel 5595  df-cnv 5596  df-co 5597  df-dm 5598  df-rn 5599  df-res 5600  df-ima 5601  df-iota 6388  df-fun 6432  df-fn 6433  df-f 6434  df-f1 6435  df-fo 6436  df-f1o 6437  df-fv 6438  df-er 8472  df-en 8708  df-dom 8709  df-sdom 8710  df-pnf 10995  df-mnf 10996  df-xr 10997  df-ltxr 10998  df-le 10999

This theorem is referenced by:  ltnsymd  11107  mulge0  11476  msqge0  11479  addgt0d  11533  lt2addd  11581  lt2msq1  11842  uzwo3  12665  fznatpl1  13292  flflp1  13508  modaddmodup  13635  expmulnbnd  13931  fzsdom2  14124  repswcshw  14506  isercolllem1  15357  caucvgrlem  15365  climcnds  15544  geomulcvg  15569  mertenslem1  15577  ruclem2  15922  ruclem12  15931  bitsfzo  16123  bitsmod  16124  lcmgcdlem  16292  isprm7  16394  4sqlem7  16626  vdwlem1  16663  met1stc  23658  cfilucfil  23696  nlmvscnlem2  23830  icccmplem2  23967  reconnlem2  23971  xrhmeo  24090  cnheibor  24099  nmoleub2lem3  24259  ipcnlem2  24389  minveclem3b  24573  ivthlem1  24596  ivthlem2  24597  ivth2  24600  ivthle  24601  ivthle2  24602  ovollb2lem  24633  ovolicc2lem4  24665  ovolicc2lem5  24666  ioombl1lem4  24706  uniioombllem4  24731  uniioombllem5  24732  opnmbllem  24746  ismbf3d  24799  mbfi1fseqlem6  24866  itg2gt0  24906  dveflem  25124  dvferm1lem  25129  dvferm2lem  25131  rollelem  25134  rolle  25135  cmvth  25136  mvth  25137  c1liplem1  25141  dvgt0lem1  25147  dvivthlem1  25153  lhop1lem  25158  lhop1  25159  dvcnvrelem1  25162  dvcnvrelem2  25163  dvcvx  25165  dgradd2  25410  aaliou3lem8  25486  aaliou3lem7  25490  ulmdvlem1  25540  itgulm  25548  radcnvlt1  25558  radcnvle  25560  abelthlem7  25578  efcvx  25589  coseq0negpitopi  25641  tangtx  25643  tanabsge  25644  tanord  25675  abslogimle  25710  divlogrlim  25771  logno1  25772  logcnlem3  25780  logcnlem4  25781  logtayl  25796  logccv  25799  cxple  25831  chordthmlem4  25966  asinsin  26023  atanlogaddlem  26044  atantan  26054  cxp2limlem  26106  logdifbnd  26124  emcllem4  26129  harmonicbnd4  26141  lgamucov  26168  ftalem1  26203  ftalem2  26204  ftalem3  26205  basellem5  26215  basellem8  26218  chpchtsum  26348  bposlem1  26413  lgseisenlem1  26504  lgsquadlem1  26509  lgsquadlem2  26510  lgsquadlem3  26511  2sqreulem1  26575  2sqreunnlem1  26578  chebbnd1lem2  26599  chebbnd1lem3  26600  chtppilimlem1  26602  chto1ub  26605  chpo1ubb  26610  vmadivsumb  26612  dchrisumlem3  26620  mulog2sumlem1  26663  vmalogdivsum2  26667  vmalogdivsum  26668  2vmadivsumlem  26669  selbergb  26678  selberg2b  26681  chpdifbndlem1  26682  selberg3lem2  26687  selberg3  26688  selberg4lem1  26689  selberg4  26690  pntrsumbnd  26695  selberg3r  26698  selberg4r  26699  selberg34r  26700  pntrlog2bndlem1  26706  pntrlog2bndlem2  26707  pntrlog2bndlem3  26708  pntrlog2bndlem4  26709  pntrlog2bndlem5  26710  pntrlog2bndlem6a  26711  pntrlog2bndlem6  26712  pntrlog2bnd  26713  pntpbnd1a  26714  pntpbnd1  26715  pntpbnd2  26716  pntibndlem2  26720  pntlemb  26726  pntlemq  26730  pntlemr  26731  pntlemj  26732  pntlemf  26734  pntlemp  26739  ostth2lem2  26763  axpaschlem  27289  axlowdimlem16  27306  smcnlem  29038  bcm1n  31095  wrdt2ind  31204  cycpmco2lem6  31377  cyc3conja  31403  smatrcl  31725  fiunelros  32121  dya2icoseg  32223  eulerpartlemgc  32308  dstfrvunirn  32420  ballotlemfc0  32438  ballotlemfcc  32439  ballotlemimin  32451  ballotlemsgt1  32456  ballotlemfrcn0  32475  sgnmul  32488  fdvposlt  32558  breprexp  32592  logdivsqrle  32609  hgt750leme  32617  tgoldbachgt  32622  lpadmax  32641  lpadright  32643  subfacval3  33130  erdszelem8  33139  cvmliftlem6  33231  cvmliftlem7  33232  cvmliftlem8  33233  cvmliftlem9  33234  cvmliftlem10  33235  sinccvglem  33609  dnibndlem9  34645  unbdqndv2lem2  34669  knoppndvlem14  34684  knoppndvlem18  34688  knoppndvlem19  34689  poimirlem7  35763  poimirlem15  35771  opnmbllem0  35792  itg2addnclem  35807  itg2addnclem3  35809  itg2addnc  35810  itg2gt0cn  35811  areacirclem1  35844  areacirc  35849  isbnd3  35921  cntotbnd  35933  rrnequiv  35972  lcmineqlem11  40027  lcmineqlem22  40038  3lexlogpow5ineq2  40043  3lexlogpow5ineq5  40048  dvrelogpow2b  40056  aks4d1p1p2  40058  aks4d1p1p4  40059  aks4d1p1p6  40061  aks4d1p1p7  40062  aks4d1p1p5  40063  aks4d1p1  40064  aks4d1p2  40065  aks4d1p3  40066  aks4d1p5  40068  aks4d1p7d1  40070  aks4d1p7  40071  aks4d1p8  40075  sticksstones6  40087  sticksstones12a  40093  sticksstones12  40094  metakunt7  40111  metakunt29  40133  metakunt30  40134  nn0rppwr  40313  nn0expgcd  40315  posqsqznn  40323  rtprmirr  40327  fltnltalem  40479  irrapxlem3  40626  pellexlem2  40632  pellfundglb  40687  monotuz  40743  monotoddzzfi  40744  acongrep  40782  cvgdvgrat  41884  hashnzfz2  41892  hashnzfzclim  41893  binomcxplemnotnn0  41927  monoords  42790  xralrple2  42847  reclt0d  42880  reclt0  42885  uzublem  42924  iooiinicc  43034  iooiinioc  43048  limciccioolb  43116  limcicciooub  43132  lptre2pt  43135  limsupubuzlem  43207  limsup10exlem  43267  icccncfext  43382  cncfiooicclem1  43388  dvdivbd  43418  dvbdfbdioolem1  43423  dvbdfbdioolem2  43424  ioodvbdlimc1lem2  43427  ioodvbdlimc2lem  43429  dvnxpaek  43437  dvnmul  43438  volioc  43467  iblspltprt  43468  itgspltprt  43474  volico  43478  volioore  43485  voliooico  43487  voliccico  43494  stoweidlem1  43496  stoweidlem3  43498  stoweidlem7  43502  stoweidlem24  43519  stoweidlem26  43521  stoweidlem42  43537  wallispilem5  43564  stirlinglem1  43569  stirlinglem6  43574  stirlinglem7  43575  stirlinglem10  43578  stirlinglem12  43580  stirlinglem13  43581  stirlingr  43585  dirkertrigeqlem1  43593  fourierdlem10  43612  fourierdlem11  43613  fourierdlem12  43614  fourierdlem14  43616  fourierdlem15  43617  fourierdlem17  43619  fourierdlem19  43621  fourierdlem30  43632  fourierdlem37  43639  fourierdlem40  43642  fourierdlem41  43643  fourierdlem42  43644  fourierdlem47  43648  fourierdlem48  43649  fourierdlem49  43650  fourierdlem50  43651  fourierdlem51  43652  fourierdlem54  43655  fourierdlem63  43664  fourierdlem64  43665  fourierdlem65  43666  fourierdlem68  43669  fourierdlem73  43674  fourierdlem74  43675  fourierdlem76  43677  fourierdlem77  43678  fourierdlem78  43679  fourierdlem79  43680  fourierdlem81  43682  fourierdlem82  43683  fourierdlem83  43684  fourierdlem92  43693  fourierdlem93  43694  fourierdlem102  43703  fourierdlem103  43704  fourierdlem104  43705  fourierdlem107  43708  fourierdlem111  43712  fourierdlem114  43715  sqwvfoura  43723  sqwvfourb  43724  fouriersw  43726  etransclem19  43748  etransclem23  43752  etransclem35  43764  etransclem41  43770  qndenserrnbllem  43789  iundjiun  43952  carageniuncllem2  44014  caratheodorylem1  44018  hoicvr  44040  ovnsubaddlem1  44062  hsphoidmvle2  44077  hoidmv1lelem1  44083  hoidmv1lelem2  44084  hoidmvlelem1  44087  hoidmvlelem2  44088  hoidmvlelem3  44089  hoiqssbllem1  44114  hoiqssbllem2  44115  volico2  44133  iinhoiicclem  44165  iunhoiioolem  44167  vonioolem2  44173  vonicclem2  44176  pimdecfgtioo  44205  pimincfltioo  44206  smflimlem4  44260  smfmullem1  44276  smflimsuplem4  44307  expnegico01  45811  eenglngeehlnmlem2  46036  inlinecirc02plem  46084