Theorem ltled 11388

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

Syntax hints:   → wi 4   ∈ wcel 2109   class class class wbr 5124  ℝcr 11133   < clt 11274   ≤ cle 11275

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2708  ax-sep 5271  ax-nul 5281  ax-pow 5340  ax-pr 5407  ax-un 7734  ax-resscn 11191  ax-pre-lttri 11208

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3062  df-rab 3421  df-v 3466  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-opab 5187  df-mpt 5207  df-id 5553  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6489  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-er 8724  df-en 8965  df-dom 8966  df-sdom 8967  df-pnf 11276  df-mnf 11277  df-xr 11278  df-ltxr 11279  df-le 11280

This theorem is referenced by:  ltnsymd  11389  mulge0  11760  msqge0  11763  addgt0d  11817  lt2addd  11865  lt2msq1  12131  uzwo3  12964  fznatpl1  13600  flflp1  13829  modaddmodup  13957  expmulnbnd  14258  fzsdom2  14451  repswcshw  14835  isercolllem1  15686  caucvgrlem  15694  climcnds  15872  geomulcvg  15897  mertenslem1  15905  ruclem2  16255  ruclem12  16264  bitsfzo  16459  bitsmod  16460  nn0rppwr  16585  nn0expgcd  16588  lcmgcdlem  16630  isprm7  16732  4sqlem7  16969  vdwlem1  17006  met1stc  24465  cfilucfil  24503  nlmvscnlem2  24629  icccmplem2  24768  reconnlem2  24772  xrhmeo  24900  cnheibor  24910  nmoleub2lem3  25071  ipcnlem2  25201  minveclem3b  25385  ivthlem1  25409  ivthlem2  25410  ivth2  25413  ivthle  25414  ivthle2  25415  ovollb2lem  25446  ovolicc2lem4  25478  ovolicc2lem5  25479  ioombl1lem4  25519  uniioombllem4  25544  uniioombllem5  25545  opnmbllem  25559  ismbf3d  25612  mbfi1fseqlem6  25678  itg2gt0  25718  dveflem  25940  dvferm1lem  25945  dvferm2lem  25947  rollelem  25950  rolle  25951  cmvth  25952  cmvthOLD  25953  mvth  25954  c1liplem1  25958  dvgt0lem1  25964  dvivthlem1  25970  lhop1lem  25975  lhop1  25976  dvcnvrelem1  25979  dvcnvrelem2  25980  dvcvx  25982  dgradd2  26231  aaliou3lem8  26310  aaliou3lem7  26314  ulmdvlem1  26366  itgulm  26374  radcnvlt1  26384  radcnvle  26386  abelthlem7  26405  efcvx  26416  coseq0negpitopi  26469  tangtx  26471  tanabsge  26472  tanord  26504  abslogimle  26539  divlogrlim  26601  logno1  26602  logcnlem3  26610  logcnlem4  26611  logtayl  26626  logccv  26629  cxple  26661  rtprmirr  26727  chordthmlem4  26802  asinsin  26859  atanlogaddlem  26880  atantan  26890  cxp2limlem  26943  logdifbnd  26961  emcllem4  26966  harmonicbnd4  26978  lgamucov  27005  ftalem1  27040  ftalem2  27041  ftalem3  27042  basellem5  27052  basellem8  27055  chpchtsum  27187  bposlem1  27252  lgseisenlem1  27343  lgsquadlem1  27348  lgsquadlem2  27349  lgsquadlem3  27350  2sqreulem1  27414  2sqreunnlem1  27417  chebbnd1lem2  27438  chebbnd1lem3  27439  chtppilimlem1  27441  chto1ub  27444  chpo1ubb  27449  vmadivsumb  27451  dchrisumlem3  27459  mulog2sumlem1  27502  vmalogdivsum2  27506  vmalogdivsum  27507  2vmadivsumlem  27508  selbergb  27517  selberg2b  27520  chpdifbndlem1  27521  selberg3lem2  27526  selberg3  27527  selberg4lem1  27528  selberg4  27529  pntrsumbnd  27534  selberg3r  27537  selberg4r  27538  selberg34r  27539  pntrlog2bndlem1  27545  pntrlog2bndlem2  27546  pntrlog2bndlem3  27547  pntrlog2bndlem4  27548  pntrlog2bndlem5  27549  pntrlog2bndlem6a  27550  pntrlog2bndlem6  27551  pntrlog2bnd  27552  pntpbnd1a  27553  pntpbnd1  27554  pntpbnd2  27555  pntibndlem2  27559  pntlemb  27565  pntlemq  27569  pntlemr  27570  pntlemj  27571  pntlemf  27573  pntlemp  27578  ostth2lem2  27602  axpaschlem  28924  axlowdimlem16  28941  smcnlem  30683  bcm1n  32777  sgnmul  32819  wrdt2ind  32934  chnub  32997  cycpmco2lem6  33147  cyc3conja  33173  smatrcl  33832  fiunelros  34210  dya2icoseg  34314  eulerpartlemgc  34399  dstfrvunirn  34512  ballotlemfc0  34530  ballotlemfcc  34531  ballotlemimin  34543  ballotlemsgt1  34548  ballotlemfrcn0  34567  fdvposlt  34636  breprexp  34670  logdivsqrle  34687  hgt750leme  34695  tgoldbachgt  34700  lpadmax  34719  lpadright  34721  subfacval3  35216  erdszelem8  35225  cvmliftlem6  35317  cvmliftlem7  35318  cvmliftlem8  35319  cvmliftlem9  35320  cvmliftlem10  35321  sinccvglem  35699  dnibndlem9  36509  unbdqndv2lem2  36533  knoppndvlem14  36548  knoppndvlem18  36552  knoppndvlem19  36553  poimirlem7  37656  poimirlem15  37664  opnmbllem0  37685  itg2addnclem  37700  itg2addnclem3  37702  itg2addnc  37703  itg2gt0cn  37704  areacirclem1  37737  areacirc  37742  isbnd3  37813  cntotbnd  37825  rrnequiv  37864  lcmineqlem11  42057  lcmineqlem22  42068  3lexlogpow5ineq2  42073  3lexlogpow5ineq5  42078  dvrelogpow2b  42086  aks4d1p1p2  42088  aks4d1p1p4  42089  aks4d1p1p6  42091  aks4d1p1p7  42092  aks4d1p1p5  42093  aks4d1p1  42094  aks4d1p2  42095  aks4d1p3  42096  aks4d1p5  42098  aks4d1p7d1  42100  aks4d1p7  42101  aks4d1p8  42105  hashscontpow1  42139  aks6d1c2lem4  42145  aks6d1c5lem2  42156  sticksstones6  42169  sticksstones12a  42175  sticksstones12  42176  aks6d1c7lem1  42198  unitscyglem2  42214  posqsqznn  42354  redvmptabs  42378  readvrec  42380  fltnltalem  42660  irrapxlem3  42822  pellexlem2  42828  pellfundglb  42883  monotuz  42940  monotoddzzfi  42941  acongrep  42979  cvgdvgrat  44312  hashnzfz2  44320  hashnzfzclim  44321  binomcxplemnotnn0  44355  monoords  45306  xralrple2  45361  reclt0d  45394  reclt0  45398  uzublem  45437  cvgcaule  45498  iooiinicc  45551  iooiinioc  45565  limciccioolb  45630  limcicciooub  45646  lptre2pt  45649  limsupubuzlem  45721  limsup10exlem  45781  icccncfext  45896  cncfiooicclem1  45902  dvdivbd  45932  dvbdfbdioolem1  45937  dvbdfbdioolem2  45938  ioodvbdlimc1lem2  45941  ioodvbdlimc2lem  45943  dvnxpaek  45951  dvnmul  45952  volioc  45981  iblspltprt  45982  itgspltprt  45988  volico  45992  volioore  45999  voliooico  46001  voliccico  46008  stoweidlem1  46010  stoweidlem3  46012  stoweidlem7  46016  stoweidlem24  46033  stoweidlem26  46035  stoweidlem42  46051  wallispilem5  46078  stirlinglem1  46083  stirlinglem6  46088  stirlinglem7  46089  stirlinglem10  46092  stirlinglem12  46094  stirlinglem13  46095  stirlingr  46099  dirkertrigeqlem1  46107  fourierdlem10  46126  fourierdlem11  46127  fourierdlem12  46128  fourierdlem14  46130  fourierdlem15  46131  fourierdlem17  46133  fourierdlem19  46135  fourierdlem30  46146  fourierdlem37  46153  fourierdlem40  46156  fourierdlem41  46157  fourierdlem42  46158  fourierdlem47  46162  fourierdlem48  46163  fourierdlem49  46164  fourierdlem50  46165  fourierdlem51  46166  fourierdlem54  46169  fourierdlem63  46178  fourierdlem64  46179  fourierdlem65  46180  fourierdlem68  46183  fourierdlem73  46188  fourierdlem74  46189  fourierdlem76  46191  fourierdlem77  46192  fourierdlem78  46193  fourierdlem79  46194  fourierdlem81  46196  fourierdlem82  46197  fourierdlem83  46198  fourierdlem92  46207  fourierdlem93  46208  fourierdlem102  46217  fourierdlem103  46218  fourierdlem104  46219  fourierdlem107  46222  fourierdlem111  46226  fourierdlem114  46229  sqwvfoura  46237  sqwvfourb  46238  fouriersw  46240  etransclem19  46262  etransclem23  46266  etransclem35  46278  etransclem41  46284  qndenserrnbllem  46303  iundjiun  46469  carageniuncllem2  46531  caratheodorylem1  46535  hoicvr  46557  ovnsubaddlem1  46579  hsphoidmvle2  46594  hoidmv1lelem1  46600  hoidmv1lelem2  46601  hoidmvlelem1  46604  hoidmvlelem2  46605  hoidmvlelem3  46606  hoiqssbllem1  46631  hoiqssbllem2  46632  volico2  46650  iinhoiicclem  46682  iunhoiioolem  46684  vonioolem2  46690  vonicclem2  46693  pimdecfgtioo  46726  pimincfltioo  46727  smflimlem4  46783  smfmullem1  46800  smflimsuplem4  46832  gpg3kgrtriexlem4  48068  gpg3kgrtriexlem6  48070  expnegico01  48474  eenglngeehlnmlem2  48698  inlinecirc02plem  48746