Theorem ltled 11325

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

Syntax hints:   → wi 4   ∈ wcel 2141   class class class wbr 5097  ℝcr 11066   < clt 11210   ≤ cle 11211

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5243  ax-nul 5253  ax-pow 5319  ax-pr 5387  ax-un 7713  ax-resscn 11124  ax-pre-lttri 11141

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3061  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-opab 5160  df-mpt 5179  df-id 5538  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656  df-iota 6472  df-fun 6518  df-fn 6519  df-f 6520  df-f1 6521  df-fo 6522  df-f1o 6523  df-fv 6524  df-er 8672  df-en 8922  df-dom 8923  df-sdom 8924  df-pnf 11212  df-mnf 11213  df-xr 11214  df-ltxr 11215  df-le 11216

This theorem is referenced by:  ltnsymd  11326  mulge0  11699  msqge0  11702  addgt0d  11756  lt2addd  11804  lt2msq1  12070  uzwo3  12938  fznatpl1  13577  flflp1  13811  modaddmodup  13941  expmulnbnd  14242  fzsdom2  14435  repswcshw  14819  sgnmul  15111  isercolllem1  15683  caucvgrlem  15691  climcnds  15872  geomulcvg  15897  mertenslem1  15905  ruclem2  16255  ruclem12  16264  bitsfzo  16460  bitsmod  16461  nn0rppwr  16586  nn0expgcd  16589  lcmgcdlem  16631  isprm7  16734  4sqlem7  16971  vdwlem1  17008  chnub  18645  met1stc  24569  cfilucfil  24607  nlmvscnlem2  24733  icccmplem2  24872  reconnlem2  24876  xrhmeo  24996  cnheibor  25005  nmoleub2lem3  25165  ipcnlem2  25294  minveclem3b  25478  ivthlem1  25501  ivthlem2  25502  ivth2  25505  ivthle  25506  ivthle2  25507  ovollb2lem  25538  ovolicc2lem4  25570  ovolicc2lem5  25571  ioombl1lem4  25611  uniioombllem4  25636  uniioombllem5  25637  opnmbllem  25651  ismbf3d  25704  mbfi1fseqlem6  25770  itg2gt0  25810  dveflem  26029  dvferm1lem  26034  dvferm2lem  26036  rollelem  26039  rolle  26040  cmvth  26041  mvth  26042  c1liplem1  26046  dvgt0lem1  26052  dvivthlem1  26058  lhop1lem  26063  lhop1  26064  dvcnvrelem1  26067  dvcnvrelem2  26068  dvcvx  26070  dgradd2  26316  aaliou3lem8  26397  aaliou3lem7  26401  ulmdvlem1  26451  itgulm  26459  radcnvlt1  26469  radcnvle  26471  abelthlem7  26489  efcvx  26500  coseq0negpitopi  26556  tangtx  26558  tanabsge  26559  tanord  26591  abslogimle  26626  divlogrlim  26688  logno1  26689  logcnlem3  26697  logcnlem4  26698  logtayl  26713  logccv  26716  cxple  26748  rtprmirr  26813  chordthmlem4  26888  asinsin  26945  atanlogaddlem  26966  atantan  26976  cxp2limlem  27028  logdifbnd  27046  emcllem4  27051  harmonicbnd4  27063  lgamucov  27090  ftalem1  27125  ftalem2  27126  ftalem3  27127  basellem5  27137  basellem8  27140  chpchtsum  27271  bposlem1  27336  lgseisenlem1  27427  lgsquadlem1  27432  lgsquadlem2  27433  lgsquadlem3  27434  2sqreulem1  27498  2sqreunnlem1  27501  chebbnd1lem2  27522  chebbnd1lem3  27523  chtppilimlem1  27525  chto1ub  27528  chpo1ubb  27533  vmadivsumb  27535  dchrisumlem3  27543  mulog2sumlem1  27586  vmalogdivsum2  27590  vmalogdivsum  27591  2vmadivsumlem  27592  selbergb  27601  selberg2b  27604  chpdifbndlem1  27605  selberg3lem2  27610  selberg3  27611  selberg4lem1  27612  selberg4  27613  pntrsumbnd  27618  selberg3r  27621  selberg4r  27622  selberg34r  27623  pntrlog2bndlem1  27629  pntrlog2bndlem2  27630  pntrlog2bndlem3  27631  pntrlog2bndlem4  27632  pntrlog2bndlem5  27633  pntrlog2bndlem6a  27634  pntrlog2bndlem6  27635  pntrlog2bnd  27636  pntpbnd1a  27637  pntpbnd1  27638  pntpbnd2  27639  pntibndlem2  27643  pntlemb  27649  pntlemq  27653  pntlemr  27654  pntlemj  27655  pntlemf  27657  pntlemp  27662  ostth2lem2  27686  axpaschlem  29098  axlowdimlem16  29115  smcnlem  30857  bcm1n  32958  wrdt2ind  33092  cycpmco2lem6  33272  cyc3conja  33298  smatrcl  34054  fiunelros  34432  dya2icoseg  34535  eulerpartlemgc  34620  dstfrvunirn  34733  ballotlemfc0  34751  ballotlemfcc  34752  ballotlemimin  34764  ballotlemsgt1  34769  ballotlemfrcn0  34788  fdvposlt  34854  breprexp  34888  logdivsqrle  34905  hgt750leme  34913  tgoldbachgt  34918  lpadmax  34940  lpadright  34942  subfacval3  35500  erdszelem8  35509  cvmliftlem6  35601  cvmliftlem7  35602  cvmliftlem8  35603  cvmliftlem9  35604  cvmliftlem10  35605  sinccvglem  35983  dnibndlem9  36885  unbdqndv2lem2  36909  knoppndvlem14  36924  knoppndvlem18  36928  knoppndvlem19  36929  poimirlem7  38087  poimirlem15  38095  opnmbllem0  38116  itg2addnclem  38131  itg2addnclem3  38133  itg2addnc  38134  itg2gt0cn  38135  areacirclem1  38168  areacirc  38173  isbnd3  38244  cntotbnd  38256  rrnequiv  38295  lcmineqlem11  42617  lcmineqlem22  42628  3lexlogpow5ineq2  42633  3lexlogpow5ineq5  42638  dvrelogpow2b  42646  aks4d1p1p2  42648  aks4d1p1p4  42649  aks4d1p1p6  42651  aks4d1p1p7  42652  aks4d1p1p5  42653  aks4d1p1  42654  aks4d1p2  42655  aks4d1p3  42656  aks4d1p5  42658  aks4d1p7d1  42660  aks4d1p7  42661  aks4d1p8  42665  hashscontpow1  42699  aks6d1c2lem4  42705  aks6d1c5lem2  42716  sticksstones6  42729  sticksstones12a  42735  sticksstones12  42736  aks6d1c7lem1  42758  unitscyglem2  42774  posqsqznn  42906  redvmptabs  42930  readvrec  42932  fltnltalem  43205  irrapxlem3  43362  pellexlem2  43368  pellfundglb  43423  monotuz  43479  monotoddzzfi  43480  acongrep  43518  cvgdvgrat  44850  hashnzfz2  44858  hashnzfzclim  44859  binomcxplemnotnn0  44893  monoords  45837  xralrple2  45891  reclt0d  45923  reclt0  45927  uzublem  45965  cvgcaule  46026  iooiinicc  46079  iooiinioc  46093  limciccioolb  46158  limcicciooub  46172  lptre2pt  46175  limsupubuzlem  46247  limsup10exlem  46307  icccncfext  46422  cncfiooicclem1  46428  dvdivbd  46458  dvbdfbdioolem1  46463  dvbdfbdioolem2  46464  ioodvbdlimc1lem2  46467  ioodvbdlimc2lem  46469  dvnxpaek  46477  dvnmul  46478  volioc  46507  iblspltprt  46508  itgspltprt  46514  volico  46518  volioore  46525  voliooico  46527  voliccico  46534  stoweidlem1  46536  stoweidlem3  46538  stoweidlem7  46542  stoweidlem24  46559  stoweidlem26  46561  stoweidlem42  46577  wallispilem5  46604  stirlinglem1  46609  stirlinglem6  46614  stirlinglem7  46615  stirlinglem10  46618  stirlinglem12  46620  stirlinglem13  46621  stirlingr  46625  dirkertrigeqlem1  46633  fourierdlem10  46652  fourierdlem11  46653  fourierdlem12  46654  fourierdlem14  46656  fourierdlem15  46657  fourierdlem17  46659  fourierdlem19  46661  fourierdlem30  46672  fourierdlem37  46679  fourierdlem40  46682  fourierdlem41  46683  fourierdlem42  46684  fourierdlem47  46688  fourierdlem48  46689  fourierdlem49  46690  fourierdlem50  46691  fourierdlem51  46692  fourierdlem54  46695  fourierdlem63  46704  fourierdlem64  46705  fourierdlem65  46706  fourierdlem68  46709  fourierdlem73  46714  fourierdlem74  46715  fourierdlem76  46717  fourierdlem77  46718  fourierdlem78  46719  fourierdlem79  46720  fourierdlem81  46722  fourierdlem82  46723  fourierdlem83  46724  fourierdlem92  46733  fourierdlem93  46734  fourierdlem102  46743  fourierdlem103  46744  fourierdlem104  46745  fourierdlem107  46748  fourierdlem111  46752  fourierdlem114  46755  sqwvfoura  46763  sqwvfourb  46764  fouriersw  46766  etransclem19  46788  etransclem23  46792  etransclem35  46804  etransclem41  46810  qndenserrnbllem  46829  iundjiun  46995  carageniuncllem2  47057  caratheodorylem1  47061  hoicvr  47083  ovnsubaddlem1  47105  hsphoidmvle2  47120  hoidmv1lelem1  47126  hoidmv1lelem2  47127  hoidmvlelem1  47130  hoidmvlelem2  47131  hoidmvlelem3  47132  hoiqssbllem1  47157  hoiqssbllem2  47158  volico2  47176  iinhoiicclem  47208  iunhoiioolem  47210  vonioolem2  47216  vonicclem2  47219  pimdecfgtioo  47252  pimincfltioo  47253  smflimlem4  47309  smfmullem1  47326  smflimsuplem4  47358  gpg3kgrtriexlem4  48669  gpg3kgrtriexlem6  48671  expnegico01  49101  eenglngeehlnmlem2  49321  inlinecirc02plem  49369