Theorem ltled 11407

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 11347	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 → 𝐴 ≤ 𝐵))
5	2, 3, 4	syl2anc 584	. 2 ⊢ (𝜑 → (𝐴 < 𝐵 → 𝐴 ≤ 𝐵))
6	1, 5	mpd 15	1 ⊢ (𝜑 → 𝐴 ≤ 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2106   class class class wbr 5148  ℝcr 11152   < clt 11293   ≤ cle 11294

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754  ax-resscn 11210  ax-pre-lttri 11227

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5583  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-er 8744  df-en 8985  df-dom 8986  df-sdom 8987  df-pnf 11295  df-mnf 11296  df-xr 11297  df-ltxr 11298  df-le 11299

This theorem is referenced by:  ltnsymd  11408  mulge0  11779  msqge0  11782  addgt0d  11836  lt2addd  11884  lt2msq1  12150  uzwo3  12983  fznatpl1  13615  flflp1  13844  modaddmodup  13972  expmulnbnd  14271  fzsdom2  14464  repswcshw  14847  isercolllem1  15698  caucvgrlem  15706  climcnds  15884  geomulcvg  15909  mertenslem1  15917  ruclem2  16265  ruclem12  16274  bitsfzo  16469  bitsmod  16470  nn0rppwr  16595  nn0expgcd  16598  lcmgcdlem  16640  isprm7  16742  4sqlem7  16978  vdwlem1  17015  met1stc  24550  cfilucfil  24588  nlmvscnlem2  24722  icccmplem2  24859  reconnlem2  24863  xrhmeo  24991  cnheibor  25001  nmoleub2lem3  25162  ipcnlem2  25292  minveclem3b  25476  ivthlem1  25500  ivthlem2  25501  ivth2  25504  ivthle  25505  ivthle2  25506  ovollb2lem  25537  ovolicc2lem4  25569  ovolicc2lem5  25570  ioombl1lem4  25610  uniioombllem4  25635  uniioombllem5  25636  opnmbllem  25650  ismbf3d  25703  mbfi1fseqlem6  25770  itg2gt0  25810  dveflem  26032  dvferm1lem  26037  dvferm2lem  26039  rollelem  26042  rolle  26043  cmvth  26044  cmvthOLD  26045  mvth  26046  c1liplem1  26050  dvgt0lem1  26056  dvivthlem1  26062  lhop1lem  26067  lhop1  26068  dvcnvrelem1  26071  dvcnvrelem2  26072  dvcvx  26074  dgradd2  26323  aaliou3lem8  26402  aaliou3lem7  26406  ulmdvlem1  26458  itgulm  26466  radcnvlt1  26476  radcnvle  26478  abelthlem7  26497  efcvx  26508  coseq0negpitopi  26560  tangtx  26562  tanabsge  26563  tanord  26595  abslogimle  26630  divlogrlim  26692  logno1  26693  logcnlem3  26701  logcnlem4  26702  logtayl  26717  logccv  26720  cxple  26752  rtprmirr  26818  chordthmlem4  26893  asinsin  26950  atanlogaddlem  26971  atantan  26981  cxp2limlem  27034  logdifbnd  27052  emcllem4  27057  harmonicbnd4  27069  lgamucov  27096  ftalem1  27131  ftalem2  27132  ftalem3  27133  basellem5  27143  basellem8  27146  chpchtsum  27278  bposlem1  27343  lgseisenlem1  27434  lgsquadlem1  27439  lgsquadlem2  27440  lgsquadlem3  27441  2sqreulem1  27505  2sqreunnlem1  27508  chebbnd1lem2  27529  chebbnd1lem3  27530  chtppilimlem1  27532  chto1ub  27535  chpo1ubb  27540  vmadivsumb  27542  dchrisumlem3  27550  mulog2sumlem1  27593  vmalogdivsum2  27597  vmalogdivsum  27598  2vmadivsumlem  27599  selbergb  27608  selberg2b  27611  chpdifbndlem1  27612  selberg3lem2  27617  selberg3  27618  selberg4lem1  27619  selberg4  27620  pntrsumbnd  27625  selberg3r  27628  selberg4r  27629  selberg34r  27630  pntrlog2bndlem1  27636  pntrlog2bndlem2  27637  pntrlog2bndlem3  27638  pntrlog2bndlem4  27639  pntrlog2bndlem5  27640  pntrlog2bndlem6a  27641  pntrlog2bndlem6  27642  pntrlog2bnd  27643  pntpbnd1a  27644  pntpbnd1  27645  pntpbnd2  27646  pntibndlem2  27650  pntlemb  27656  pntlemq  27660  pntlemr  27661  pntlemj  27662  pntlemf  27664  pntlemp  27669  ostth2lem2  27693  axpaschlem  28970  axlowdimlem16  28987  smcnlem  30726  bcm1n  32803  wrdt2ind  32923  chnub  32986  cycpmco2lem6  33134  cyc3conja  33160  smatrcl  33757  fiunelros  34155  dya2icoseg  34259  eulerpartlemgc  34344  dstfrvunirn  34456  ballotlemfc0  34474  ballotlemfcc  34475  ballotlemimin  34487  ballotlemsgt1  34492  ballotlemfrcn0  34511  sgnmul  34524  fdvposlt  34593  breprexp  34627  logdivsqrle  34644  hgt750leme  34652  tgoldbachgt  34657  lpadmax  34676  lpadright  34678  subfacval3  35174  erdszelem8  35183  cvmliftlem6  35275  cvmliftlem7  35276  cvmliftlem8  35277  cvmliftlem9  35278  cvmliftlem10  35279  sinccvglem  35657  dnibndlem9  36469  unbdqndv2lem2  36493  knoppndvlem14  36508  knoppndvlem18  36512  knoppndvlem19  36513  poimirlem7  37614  poimirlem15  37622  opnmbllem0  37643  itg2addnclem  37658  itg2addnclem3  37660  itg2addnc  37661  itg2gt0cn  37662  areacirclem1  37695  areacirc  37700  isbnd3  37771  cntotbnd  37783  rrnequiv  37822  lcmineqlem11  42021  lcmineqlem22  42032  3lexlogpow5ineq2  42037  3lexlogpow5ineq5  42042  dvrelogpow2b  42050  aks4d1p1p2  42052  aks4d1p1p4  42053  aks4d1p1p6  42055  aks4d1p1p7  42056  aks4d1p1p5  42057  aks4d1p1  42058  aks4d1p2  42059  aks4d1p3  42060  aks4d1p5  42062  aks4d1p7d1  42064  aks4d1p7  42065  aks4d1p8  42069  hashscontpow1  42103  aks6d1c2lem4  42109  aks6d1c5lem2  42120  sticksstones6  42133  sticksstones12a  42139  sticksstones12  42140  aks6d1c7lem1  42162  unitscyglem2  42178  metakunt7  42193  metakunt29  42215  metakunt30  42216  posqsqznn  42350  redvmptabs  42369  readvrec  42371  fltnltalem  42649  irrapxlem3  42812  pellexlem2  42818  pellfundglb  42873  monotuz  42930  monotoddzzfi  42931  acongrep  42969  cvgdvgrat  44309  hashnzfz2  44317  hashnzfzclim  44318  binomcxplemnotnn0  44352  monoords  45248  xralrple2  45304  reclt0d  45337  reclt0  45341  uzublem  45380  cvgcaule  45442  iooiinicc  45495  iooiinioc  45509  limciccioolb  45577  limcicciooub  45593  lptre2pt  45596  limsupubuzlem  45668  limsup10exlem  45728  icccncfext  45843  cncfiooicclem1  45849  dvdivbd  45879  dvbdfbdioolem1  45884  dvbdfbdioolem2  45885  ioodvbdlimc1lem2  45888  ioodvbdlimc2lem  45890  dvnxpaek  45898  dvnmul  45899  volioc  45928  iblspltprt  45929  itgspltprt  45935  volico  45939  volioore  45946  voliooico  45948  voliccico  45955  stoweidlem1  45957  stoweidlem3  45959  stoweidlem7  45963  stoweidlem24  45980  stoweidlem26  45982  stoweidlem42  45998  wallispilem5  46025  stirlinglem1  46030  stirlinglem6  46035  stirlinglem7  46036  stirlinglem10  46039  stirlinglem12  46041  stirlinglem13  46042  stirlingr  46046  dirkertrigeqlem1  46054  fourierdlem10  46073  fourierdlem11  46074  fourierdlem12  46075  fourierdlem14  46077  fourierdlem15  46078  fourierdlem17  46080  fourierdlem19  46082  fourierdlem30  46093  fourierdlem37  46100  fourierdlem40  46103  fourierdlem41  46104  fourierdlem42  46105  fourierdlem47  46109  fourierdlem48  46110  fourierdlem49  46111  fourierdlem50  46112  fourierdlem51  46113  fourierdlem54  46116  fourierdlem63  46125  fourierdlem64  46126  fourierdlem65  46127  fourierdlem68  46130  fourierdlem73  46135  fourierdlem74  46136  fourierdlem76  46138  fourierdlem77  46139  fourierdlem78  46140  fourierdlem79  46141  fourierdlem81  46143  fourierdlem82  46144  fourierdlem83  46145  fourierdlem92  46154  fourierdlem93  46155  fourierdlem102  46164  fourierdlem103  46165  fourierdlem104  46166  fourierdlem107  46169  fourierdlem111  46173  fourierdlem114  46176  sqwvfoura  46184  sqwvfourb  46185  fouriersw  46187  etransclem19  46209  etransclem23  46213  etransclem35  46225  etransclem41  46231  qndenserrnbllem  46250  iundjiun  46416  carageniuncllem2  46478  caratheodorylem1  46482  hoicvr  46504  ovnsubaddlem1  46526  hsphoidmvle2  46541  hoidmv1lelem1  46547  hoidmv1lelem2  46548  hoidmvlelem1  46551  hoidmvlelem2  46552  hoidmvlelem3  46553  hoiqssbllem1  46578  hoiqssbllem2  46579  volico2  46597  iinhoiicclem  46629  iunhoiioolem  46631  vonioolem2  46637  vonicclem2  46640  pimdecfgtioo  46673  pimincfltioo  46674  smflimlem4  46730  smfmullem1  46747  smflimsuplem4  46779  expnegico01  48364  eenglngeehlnmlem2  48588  inlinecirc02plem  48636