Theorem ltled 11285

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

Syntax hints:   → wi 4   ∈ wcel 2119   class class class wbr 5072  ℝcr 11028   < clt 11170   ≤ cle 11171

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pow 5294  ax-pr 5362  ax-un 7678  ax-resscn 11086  ax-pre-lttri 11103

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-nel 3039  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-opab 5135  df-mpt 5154  df-id 5513  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493  df-er 8633  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176

This theorem is referenced by:  ltnsymd  11286  mulge0  11659  msqge0  11662  addgt0d  11716  lt2addd  11764  lt2msq1  12031  uzwo3  12884  fznatpl1  13523  flflp1  13757  modaddmodup  13887  expmulnbnd  14188  fzsdom2  14381  repswcshw  14765  isercolllem1  15618  caucvgrlem  15626  climcnds  15807  geomulcvg  15832  mertenslem1  15840  ruclem2  16190  ruclem12  16199  bitsfzo  16395  bitsmod  16396  nn0rppwr  16521  nn0expgcd  16524  lcmgcdlem  16566  isprm7  16669  4sqlem7  16906  vdwlem1  16943  chnub  18579  met1stc  24504  cfilucfil  24542  nlmvscnlem2  24668  icccmplem2  24807  reconnlem2  24811  xrhmeo  24931  cnheibor  24940  nmoleub2lem3  25100  ipcnlem2  25229  minveclem3b  25413  ivthlem1  25436  ivthlem2  25437  ivth2  25440  ivthle  25441  ivthle2  25442  ovollb2lem  25473  ovolicc2lem4  25505  ovolicc2lem5  25506  ioombl1lem4  25546  uniioombllem4  25571  uniioombllem5  25572  opnmbllem  25586  ismbf3d  25639  mbfi1fseqlem6  25705  itg2gt0  25745  dveflem  25964  dvferm1lem  25969  dvferm2lem  25971  rollelem  25974  rolle  25975  cmvth  25976  mvth  25977  c1liplem1  25981  dvgt0lem1  25987  dvivthlem1  25993  lhop1lem  25998  lhop1  25999  dvcnvrelem1  26002  dvcnvrelem2  26003  dvcvx  26005  dgradd2  26251  aaliou3lem8  26329  aaliou3lem7  26333  ulmdvlem1  26383  itgulm  26391  radcnvlt1  26401  radcnvle  26403  abelthlem7  26421  efcvx  26432  coseq0negpitopi  26485  tangtx  26487  tanabsge  26488  tanord  26520  abslogimle  26555  divlogrlim  26617  logno1  26618  logcnlem3  26626  logcnlem4  26627  logtayl  26642  logccv  26645  cxple  26677  rtprmirr  26742  chordthmlem4  26817  asinsin  26874  atanlogaddlem  26895  atantan  26905  cxp2limlem  26957  logdifbnd  26975  emcllem4  26980  harmonicbnd4  26992  lgamucov  27019  ftalem1  27054  ftalem2  27055  ftalem3  27056  basellem5  27066  basellem8  27069  chpchtsum  27200  bposlem1  27265  lgseisenlem1  27356  lgsquadlem1  27361  lgsquadlem2  27362  lgsquadlem3  27363  2sqreulem1  27427  2sqreunnlem1  27430  chebbnd1lem2  27451  chebbnd1lem3  27452  chtppilimlem1  27454  chto1ub  27457  chpo1ubb  27462  vmadivsumb  27464  dchrisumlem3  27472  mulog2sumlem1  27515  vmalogdivsum2  27519  vmalogdivsum  27520  2vmadivsumlem  27521  selbergb  27530  selberg2b  27533  chpdifbndlem1  27534  selberg3lem2  27539  selberg3  27540  selberg4lem1  27541  selberg4  27542  pntrsumbnd  27547  selberg3r  27550  selberg4r  27551  selberg34r  27552  pntrlog2bndlem1  27558  pntrlog2bndlem2  27559  pntrlog2bndlem3  27560  pntrlog2bndlem4  27561  pntrlog2bndlem5  27562  pntrlog2bndlem6a  27563  pntrlog2bndlem6  27564  pntrlog2bnd  27565  pntpbnd1a  27566  pntpbnd1  27567  pntpbnd2  27568  pntibndlem2  27572  pntlemb  27578  pntlemq  27582  pntlemr  27583  pntlemj  27584  pntlemf  27586  pntlemp  27591  ostth2lem2  27615  axpaschlem  29027  axlowdimlem16  29044  smcnlem  30786  bcm1n  32887  sgnmul  32927  wrdt2ind  33032  cycpmco2lem6  33212  cyc3conja  33238  smatrcl  33980  fiunelros  34358  dya2icoseg  34461  eulerpartlemgc  34546  dstfrvunirn  34659  ballotlemfc0  34677  ballotlemfcc  34678  ballotlemimin  34690  ballotlemsgt1  34695  ballotlemfrcn0  34714  fdvposlt  34783  breprexp  34817  logdivsqrle  34834  hgt750leme  34842  tgoldbachgt  34847  lpadmax  34866  lpadright  34868  subfacval3  35417  erdszelem8  35426  cvmliftlem6  35518  cvmliftlem7  35519  cvmliftlem8  35520  cvmliftlem9  35521  cvmliftlem10  35522  sinccvglem  35900  dnibndlem9  36792  unbdqndv2lem2  36816  knoppndvlem14  36831  knoppndvlem18  36835  knoppndvlem19  36836  poimirlem7  37994  poimirlem15  38002  opnmbllem0  38023  itg2addnclem  38038  itg2addnclem3  38040  itg2addnc  38041  itg2gt0cn  38042  areacirclem1  38075  areacirc  38080  isbnd3  38151  cntotbnd  38163  rrnequiv  38202  lcmineqlem11  42524  lcmineqlem22  42535  3lexlogpow5ineq2  42540  3lexlogpow5ineq5  42545  dvrelogpow2b  42553  aks4d1p1p2  42555  aks4d1p1p4  42556  aks4d1p1p6  42558  aks4d1p1p7  42559  aks4d1p1p5  42560  aks4d1p1  42561  aks4d1p2  42562  aks4d1p3  42563  aks4d1p5  42565  aks4d1p7d1  42567  aks4d1p7  42568  aks4d1p8  42572  hashscontpow1  42606  aks6d1c2lem4  42612  aks6d1c5lem2  42623  sticksstones6  42636  sticksstones12a  42642  sticksstones12  42643  aks6d1c7lem1  42665  unitscyglem2  42681  posqsqznn  42813  redvmptabs  42837  readvrec  42839  fltnltalem  43112  irrapxlem3  43269  pellexlem2  43275  pellfundglb  43330  monotuz  43386  monotoddzzfi  43387  acongrep  43425  cvgdvgrat  44757  hashnzfz2  44765  hashnzfzclim  44766  binomcxplemnotnn0  44800  monoords  45745  xralrple2  45799  reclt0d  45831  reclt0  45835  uzublem  45873  cvgcaule  45934  iooiinicc  45987  iooiinioc  46001  limciccioolb  46066  limcicciooub  46080  lptre2pt  46083  limsupubuzlem  46155  limsup10exlem  46215  icccncfext  46330  cncfiooicclem1  46336  dvdivbd  46366  dvbdfbdioolem1  46371  dvbdfbdioolem2  46372  ioodvbdlimc1lem2  46375  ioodvbdlimc2lem  46377  dvnxpaek  46385  dvnmul  46386  volioc  46415  iblspltprt  46416  itgspltprt  46422  volico  46426  volioore  46433  voliooico  46435  voliccico  46442  stoweidlem1  46444  stoweidlem3  46446  stoweidlem7  46450  stoweidlem24  46467  stoweidlem26  46469  stoweidlem42  46485  wallispilem5  46512  stirlinglem1  46517  stirlinglem6  46522  stirlinglem7  46523  stirlinglem10  46526  stirlinglem12  46528  stirlinglem13  46529  stirlingr  46533  dirkertrigeqlem1  46541  fourierdlem10  46560  fourierdlem11  46561  fourierdlem12  46562  fourierdlem14  46564  fourierdlem15  46565  fourierdlem17  46567  fourierdlem19  46569  fourierdlem30  46580  fourierdlem37  46587  fourierdlem40  46590  fourierdlem41  46591  fourierdlem42  46592  fourierdlem47  46596  fourierdlem48  46597  fourierdlem49  46598  fourierdlem50  46599  fourierdlem51  46600  fourierdlem54  46603  fourierdlem63  46612  fourierdlem64  46613  fourierdlem65  46614  fourierdlem68  46617  fourierdlem73  46622  fourierdlem74  46623  fourierdlem76  46625  fourierdlem77  46626  fourierdlem78  46627  fourierdlem79  46628  fourierdlem81  46630  fourierdlem82  46631  fourierdlem83  46632  fourierdlem92  46641  fourierdlem93  46642  fourierdlem102  46651  fourierdlem103  46652  fourierdlem104  46653  fourierdlem107  46656  fourierdlem111  46660  fourierdlem114  46663  sqwvfoura  46671  sqwvfourb  46672  fouriersw  46674  etransclem19  46696  etransclem23  46700  etransclem35  46712  etransclem41  46718  qndenserrnbllem  46737  iundjiun  46903  carageniuncllem2  46965  caratheodorylem1  46969  hoicvr  46991  ovnsubaddlem1  47013  hsphoidmvle2  47028  hoidmv1lelem1  47034  hoidmv1lelem2  47035  hoidmvlelem1  47038  hoidmvlelem2  47039  hoidmvlelem3  47040  hoiqssbllem1  47065  hoiqssbllem2  47066  volico2  47084  iinhoiicclem  47116  iunhoiioolem  47118  vonioolem2  47124  vonicclem2  47127  pimdecfgtioo  47160  pimincfltioo  47161  smflimlem4  47217  smfmullem1  47234  smflimsuplem4  47266  gpg3kgrtriexlem4  48577  gpg3kgrtriexlem6  48579  expnegico01  49009  eenglngeehlnmlem2  49229  inlinecirc02plem  49277