Theorem ltled 11282

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

Syntax hints:   → wi 4   ∈ wcel 2109   class class class wbr 5095  ℝcr 11027   < clt 11168   ≤ cle 11169

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 2701  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7675  ax-resscn 11085  ax-pre-lttri 11102

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 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5518  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-er 8632  df-en 8880  df-dom 8881  df-sdom 8882  df-pnf 11170  df-mnf 11171  df-xr 11172  df-ltxr 11173  df-le 11174

This theorem is referenced by:  ltnsymd  11283  mulge0  11656  msqge0  11659  addgt0d  11713  lt2addd  11761  lt2msq1  12027  uzwo3  12862  fznatpl1  13499  flflp1  13729  modaddmodup  13859  expmulnbnd  14160  fzsdom2  14353  repswcshw  14736  isercolllem1  15590  caucvgrlem  15598  climcnds  15776  geomulcvg  15801  mertenslem1  15809  ruclem2  16159  ruclem12  16168  bitsfzo  16364  bitsmod  16365  nn0rppwr  16490  nn0expgcd  16493  lcmgcdlem  16535  isprm7  16637  4sqlem7  16874  vdwlem1  16911  met1stc  24425  cfilucfil  24463  nlmvscnlem2  24589  icccmplem2  24728  reconnlem2  24732  xrhmeo  24860  cnheibor  24870  nmoleub2lem3  25031  ipcnlem2  25160  minveclem3b  25344  ivthlem1  25368  ivthlem2  25369  ivth2  25372  ivthle  25373  ivthle2  25374  ovollb2lem  25405  ovolicc2lem4  25437  ovolicc2lem5  25438  ioombl1lem4  25478  uniioombllem4  25503  uniioombllem5  25504  opnmbllem  25518  ismbf3d  25571  mbfi1fseqlem6  25637  itg2gt0  25677  dveflem  25899  dvferm1lem  25904  dvferm2lem  25906  rollelem  25909  rolle  25910  cmvth  25911  cmvthOLD  25912  mvth  25913  c1liplem1  25917  dvgt0lem1  25923  dvivthlem1  25929  lhop1lem  25934  lhop1  25935  dvcnvrelem1  25938  dvcnvrelem2  25939  dvcvx  25941  dgradd2  26190  aaliou3lem8  26269  aaliou3lem7  26273  ulmdvlem1  26325  itgulm  26333  radcnvlt1  26343  radcnvle  26345  abelthlem7  26364  efcvx  26375  coseq0negpitopi  26428  tangtx  26430  tanabsge  26431  tanord  26463  abslogimle  26498  divlogrlim  26560  logno1  26561  logcnlem3  26569  logcnlem4  26570  logtayl  26585  logccv  26588  cxple  26620  rtprmirr  26686  chordthmlem4  26761  asinsin  26818  atanlogaddlem  26839  atantan  26849  cxp2limlem  26902  logdifbnd  26920  emcllem4  26925  harmonicbnd4  26937  lgamucov  26964  ftalem1  26999  ftalem2  27000  ftalem3  27001  basellem5  27011  basellem8  27014  chpchtsum  27146  bposlem1  27211  lgseisenlem1  27302  lgsquadlem1  27307  lgsquadlem2  27308  lgsquadlem3  27309  2sqreulem1  27373  2sqreunnlem1  27376  chebbnd1lem2  27397  chebbnd1lem3  27398  chtppilimlem1  27400  chto1ub  27403  chpo1ubb  27408  vmadivsumb  27410  dchrisumlem3  27418  mulog2sumlem1  27461  vmalogdivsum2  27465  vmalogdivsum  27466  2vmadivsumlem  27467  selbergb  27476  selberg2b  27479  chpdifbndlem1  27480  selberg3lem2  27485  selberg3  27486  selberg4lem1  27487  selberg4  27488  pntrsumbnd  27493  selberg3r  27496  selberg4r  27497  selberg34r  27498  pntrlog2bndlem1  27504  pntrlog2bndlem2  27505  pntrlog2bndlem3  27506  pntrlog2bndlem4  27507  pntrlog2bndlem5  27508  pntrlog2bndlem6a  27509  pntrlog2bndlem6  27510  pntrlog2bnd  27511  pntpbnd1a  27512  pntpbnd1  27513  pntpbnd2  27514  pntibndlem2  27518  pntlemb  27524  pntlemq  27528  pntlemr  27529  pntlemj  27530  pntlemf  27532  pntlemp  27537  ostth2lem2  27561  axpaschlem  28903  axlowdimlem16  28920  smcnlem  30659  bcm1n  32751  sgnmul  32793  wrdt2ind  32908  chnub  32967  cycpmco2lem6  33086  cyc3conja  33112  smatrcl  33765  fiunelros  34143  dya2icoseg  34247  eulerpartlemgc  34332  dstfrvunirn  34445  ballotlemfc0  34463  ballotlemfcc  34464  ballotlemimin  34476  ballotlemsgt1  34481  ballotlemfrcn0  34500  fdvposlt  34569  breprexp  34603  logdivsqrle  34620  hgt750leme  34628  tgoldbachgt  34633  lpadmax  34652  lpadright  34654  subfacval3  35164  erdszelem8  35173  cvmliftlem6  35265  cvmliftlem7  35266  cvmliftlem8  35267  cvmliftlem9  35268  cvmliftlem10  35269  sinccvglem  35647  dnibndlem9  36462  unbdqndv2lem2  36486  knoppndvlem14  36501  knoppndvlem18  36505  knoppndvlem19  36506  poimirlem7  37609  poimirlem15  37617  opnmbllem0  37638  itg2addnclem  37653  itg2addnclem3  37655  itg2addnc  37656  itg2gt0cn  37657  areacirclem1  37690  areacirc  37695  isbnd3  37766  cntotbnd  37778  rrnequiv  37817  lcmineqlem11  42015  lcmineqlem22  42026  3lexlogpow5ineq2  42031  3lexlogpow5ineq5  42036  dvrelogpow2b  42044  aks4d1p1p2  42046  aks4d1p1p4  42047  aks4d1p1p6  42049  aks4d1p1p7  42050  aks4d1p1p5  42051  aks4d1p1  42052  aks4d1p2  42053  aks4d1p3  42054  aks4d1p5  42056  aks4d1p7d1  42058  aks4d1p7  42059  aks4d1p8  42063  hashscontpow1  42097  aks6d1c2lem4  42103  aks6d1c5lem2  42114  sticksstones6  42127  sticksstones12a  42133  sticksstones12  42134  aks6d1c7lem1  42156  unitscyglem2  42172  posqsqznn  42312  redvmptabs  42336  readvrec  42338  fltnltalem  42638  irrapxlem3  42800  pellexlem2  42806  pellfundglb  42861  monotuz  42917  monotoddzzfi  42918  acongrep  42956  cvgdvgrat  44289  hashnzfz2  44297  hashnzfzclim  44298  binomcxplemnotnn0  44332  monoords  45282  xralrple2  45337  reclt0d  45370  reclt0  45374  uzublem  45413  cvgcaule  45474  iooiinicc  45527  iooiinioc  45541  limciccioolb  45606  limcicciooub  45622  lptre2pt  45625  limsupubuzlem  45697  limsup10exlem  45757  icccncfext  45872  cncfiooicclem1  45878  dvdivbd  45908  dvbdfbdioolem1  45913  dvbdfbdioolem2  45914  ioodvbdlimc1lem2  45917  ioodvbdlimc2lem  45919  dvnxpaek  45927  dvnmul  45928  volioc  45957  iblspltprt  45958  itgspltprt  45964  volico  45968  volioore  45975  voliooico  45977  voliccico  45984  stoweidlem1  45986  stoweidlem3  45988  stoweidlem7  45992  stoweidlem24  46009  stoweidlem26  46011  stoweidlem42  46027  wallispilem5  46054  stirlinglem1  46059  stirlinglem6  46064  stirlinglem7  46065  stirlinglem10  46068  stirlinglem12  46070  stirlinglem13  46071  stirlingr  46075  dirkertrigeqlem1  46083  fourierdlem10  46102  fourierdlem11  46103  fourierdlem12  46104  fourierdlem14  46106  fourierdlem15  46107  fourierdlem17  46109  fourierdlem19  46111  fourierdlem30  46122  fourierdlem37  46129  fourierdlem40  46132  fourierdlem41  46133  fourierdlem42  46134  fourierdlem47  46138  fourierdlem48  46139  fourierdlem49  46140  fourierdlem50  46141  fourierdlem51  46142  fourierdlem54  46145  fourierdlem63  46154  fourierdlem64  46155  fourierdlem65  46156  fourierdlem68  46159  fourierdlem73  46164  fourierdlem74  46165  fourierdlem76  46167  fourierdlem77  46168  fourierdlem78  46169  fourierdlem79  46170  fourierdlem81  46172  fourierdlem82  46173  fourierdlem83  46174  fourierdlem92  46183  fourierdlem93  46184  fourierdlem102  46193  fourierdlem103  46194  fourierdlem104  46195  fourierdlem107  46198  fourierdlem111  46202  fourierdlem114  46205  sqwvfoura  46213  sqwvfourb  46214  fouriersw  46216  etransclem19  46238  etransclem23  46242  etransclem35  46254  etransclem41  46260  qndenserrnbllem  46279  iundjiun  46445  carageniuncllem2  46507  caratheodorylem1  46511  hoicvr  46533  ovnsubaddlem1  46555  hsphoidmvle2  46570  hoidmv1lelem1  46576  hoidmv1lelem2  46577  hoidmvlelem1  46580  hoidmvlelem2  46581  hoidmvlelem3  46582  hoiqssbllem1  46607  hoiqssbllem2  46608  volico2  46626  iinhoiicclem  46658  iunhoiioolem  46660  vonioolem2  46666  vonicclem2  46669  pimdecfgtioo  46702  pimincfltioo  46703  smflimlem4  46759  smfmullem1  46776  smflimsuplem4  46808  gpg3kgrtriexlem4  48074  gpg3kgrtriexlem6  48076  expnegico01  48507  eenglngeehlnmlem2  48727  inlinecirc02plem  48775