Theorem ltled 11261

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

Syntax hints:   → wi 4   ∈ wcel 2111   class class class wbr 5089  ℝcr 11005   < clt 11146   ≤ cle 11147

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pow 5301  ax-pr 5368  ax-un 7668  ax-resscn 11063  ax-pre-lttri 11080

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-nel 3033  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4281  df-if 4473  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-opab 5152  df-mpt 5171  df-id 5509  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488  df-fv 6489  df-er 8622  df-en 8870  df-dom 8871  df-sdom 8872  df-pnf 11148  df-mnf 11149  df-xr 11150  df-ltxr 11151  df-le 11152

This theorem is referenced by:  ltnsymd  11262  mulge0  11635  msqge0  11638  addgt0d  11692  lt2addd  11740  lt2msq1  12006  uzwo3  12841  fznatpl1  13478  flflp1  13711  modaddmodup  13841  expmulnbnd  14142  fzsdom2  14335  repswcshw  14719  isercolllem1  15572  caucvgrlem  15580  climcnds  15758  geomulcvg  15783  mertenslem1  15791  ruclem2  16141  ruclem12  16150  bitsfzo  16346  bitsmod  16347  nn0rppwr  16472  nn0expgcd  16475  lcmgcdlem  16517  isprm7  16619  4sqlem7  16856  vdwlem1  16893  chnub  18528  met1stc  24436  cfilucfil  24474  nlmvscnlem2  24600  icccmplem2  24739  reconnlem2  24743  xrhmeo  24871  cnheibor  24881  nmoleub2lem3  25042  ipcnlem2  25171  minveclem3b  25355  ivthlem1  25379  ivthlem2  25380  ivth2  25383  ivthle  25384  ivthle2  25385  ovollb2lem  25416  ovolicc2lem4  25448  ovolicc2lem5  25449  ioombl1lem4  25489  uniioombllem4  25514  uniioombllem5  25515  opnmbllem  25529  ismbf3d  25582  mbfi1fseqlem6  25648  itg2gt0  25688  dveflem  25910  dvferm1lem  25915  dvferm2lem  25917  rollelem  25920  rolle  25921  cmvth  25922  cmvthOLD  25923  mvth  25924  c1liplem1  25928  dvgt0lem1  25934  dvivthlem1  25940  lhop1lem  25945  lhop1  25946  dvcnvrelem1  25949  dvcnvrelem2  25950  dvcvx  25952  dgradd2  26201  aaliou3lem8  26280  aaliou3lem7  26284  ulmdvlem1  26336  itgulm  26344  radcnvlt1  26354  radcnvle  26356  abelthlem7  26375  efcvx  26386  coseq0negpitopi  26439  tangtx  26441  tanabsge  26442  tanord  26474  abslogimle  26509  divlogrlim  26571  logno1  26572  logcnlem3  26580  logcnlem4  26581  logtayl  26596  logccv  26599  cxple  26631  rtprmirr  26697  chordthmlem4  26772  asinsin  26829  atanlogaddlem  26850  atantan  26860  cxp2limlem  26913  logdifbnd  26931  emcllem4  26936  harmonicbnd4  26948  lgamucov  26975  ftalem1  27010  ftalem2  27011  ftalem3  27012  basellem5  27022  basellem8  27025  chpchtsum  27157  bposlem1  27222  lgseisenlem1  27313  lgsquadlem1  27318  lgsquadlem2  27319  lgsquadlem3  27320  2sqreulem1  27384  2sqreunnlem1  27387  chebbnd1lem2  27408  chebbnd1lem3  27409  chtppilimlem1  27411  chto1ub  27414  chpo1ubb  27419  vmadivsumb  27421  dchrisumlem3  27429  mulog2sumlem1  27472  vmalogdivsum2  27476  vmalogdivsum  27477  2vmadivsumlem  27478  selbergb  27487  selberg2b  27490  chpdifbndlem1  27491  selberg3lem2  27496  selberg3  27497  selberg4lem1  27498  selberg4  27499  pntrsumbnd  27504  selberg3r  27507  selberg4r  27508  selberg34r  27509  pntrlog2bndlem1  27515  pntrlog2bndlem2  27516  pntrlog2bndlem3  27517  pntrlog2bndlem4  27518  pntrlog2bndlem5  27519  pntrlog2bndlem6a  27520  pntrlog2bndlem6  27521  pntrlog2bnd  27522  pntpbnd1a  27523  pntpbnd1  27524  pntpbnd2  27525  pntibndlem2  27529  pntlemb  27535  pntlemq  27539  pntlemr  27540  pntlemj  27541  pntlemf  27543  pntlemp  27548  ostth2lem2  27572  axpaschlem  28918  axlowdimlem16  28935  smcnlem  30677  bcm1n  32777  sgnmul  32818  wrdt2ind  32934  cycpmco2lem6  33100  cyc3conja  33126  smatrcl  33809  fiunelros  34187  dya2icoseg  34290  eulerpartlemgc  34375  dstfrvunirn  34488  ballotlemfc0  34506  ballotlemfcc  34507  ballotlemimin  34519  ballotlemsgt1  34524  ballotlemfrcn0  34543  fdvposlt  34612  breprexp  34646  logdivsqrle  34663  hgt750leme  34671  tgoldbachgt  34676  lpadmax  34695  lpadright  34697  subfacval3  35233  erdszelem8  35242  cvmliftlem6  35334  cvmliftlem7  35335  cvmliftlem8  35336  cvmliftlem9  35337  cvmliftlem10  35338  sinccvglem  35716  dnibndlem9  36530  unbdqndv2lem2  36554  knoppndvlem14  36569  knoppndvlem18  36573  knoppndvlem19  36574  poimirlem7  37666  poimirlem15  37674  opnmbllem0  37695  itg2addnclem  37710  itg2addnclem3  37712  itg2addnc  37713  itg2gt0cn  37714  areacirclem1  37747  areacirc  37752  isbnd3  37823  cntotbnd  37835  rrnequiv  37874  lcmineqlem11  42131  lcmineqlem22  42142  3lexlogpow5ineq2  42147  3lexlogpow5ineq5  42152  dvrelogpow2b  42160  aks4d1p1p2  42162  aks4d1p1p4  42163  aks4d1p1p6  42165  aks4d1p1p7  42166  aks4d1p1p5  42167  aks4d1p1  42168  aks4d1p2  42169  aks4d1p3  42170  aks4d1p5  42172  aks4d1p7d1  42174  aks4d1p7  42175  aks4d1p8  42179  hashscontpow1  42213  aks6d1c2lem4  42219  aks6d1c5lem2  42230  sticksstones6  42243  sticksstones12a  42249  sticksstones12  42250  aks6d1c7lem1  42272  unitscyglem2  42288  posqsqznn  42428  redvmptabs  42452  readvrec  42454  fltnltalem  42754  irrapxlem3  42916  pellexlem2  42922  pellfundglb  42977  monotuz  43033  monotoddzzfi  43034  acongrep  43072  cvgdvgrat  44405  hashnzfz2  44413  hashnzfzclim  44414  binomcxplemnotnn0  44448  monoords  45397  xralrple2  45452  reclt0d  45484  reclt0  45488  uzublem  45527  cvgcaule  45588  iooiinicc  45641  iooiinioc  45655  limciccioolb  45720  limcicciooub  45734  lptre2pt  45737  limsupubuzlem  45809  limsup10exlem  45869  icccncfext  45984  cncfiooicclem1  45990  dvdivbd  46020  dvbdfbdioolem1  46025  dvbdfbdioolem2  46026  ioodvbdlimc1lem2  46029  ioodvbdlimc2lem  46031  dvnxpaek  46039  dvnmul  46040  volioc  46069  iblspltprt  46070  itgspltprt  46076  volico  46080  volioore  46087  voliooico  46089  voliccico  46096  stoweidlem1  46098  stoweidlem3  46100  stoweidlem7  46104  stoweidlem24  46121  stoweidlem26  46123  stoweidlem42  46139  wallispilem5  46166  stirlinglem1  46171  stirlinglem6  46176  stirlinglem7  46177  stirlinglem10  46180  stirlinglem12  46182  stirlinglem13  46183  stirlingr  46187  dirkertrigeqlem1  46195  fourierdlem10  46214  fourierdlem11  46215  fourierdlem12  46216  fourierdlem14  46218  fourierdlem15  46219  fourierdlem17  46221  fourierdlem19  46223  fourierdlem30  46234  fourierdlem37  46241  fourierdlem40  46244  fourierdlem41  46245  fourierdlem42  46246  fourierdlem47  46250  fourierdlem48  46251  fourierdlem49  46252  fourierdlem50  46253  fourierdlem51  46254  fourierdlem54  46257  fourierdlem63  46266  fourierdlem64  46267  fourierdlem65  46268  fourierdlem68  46271  fourierdlem73  46276  fourierdlem74  46277  fourierdlem76  46279  fourierdlem77  46280  fourierdlem78  46281  fourierdlem79  46282  fourierdlem81  46284  fourierdlem82  46285  fourierdlem83  46286  fourierdlem92  46295  fourierdlem93  46296  fourierdlem102  46305  fourierdlem103  46306  fourierdlem104  46307  fourierdlem107  46310  fourierdlem111  46314  fourierdlem114  46317  sqwvfoura  46325  sqwvfourb  46326  fouriersw  46328  etransclem19  46350  etransclem23  46354  etransclem35  46366  etransclem41  46372  qndenserrnbllem  46391  iundjiun  46557  carageniuncllem2  46619  caratheodorylem1  46623  hoicvr  46645  ovnsubaddlem1  46667  hsphoidmvle2  46682  hoidmv1lelem1  46688  hoidmv1lelem2  46689  hoidmvlelem1  46692  hoidmvlelem2  46693  hoidmvlelem3  46694  hoiqssbllem1  46719  hoiqssbllem2  46720  volico2  46738  iinhoiicclem  46770  iunhoiioolem  46772  vonioolem2  46778  vonicclem2  46781  pimdecfgtioo  46814  pimincfltioo  46815  smflimlem4  46871  smfmullem1  46888  smflimsuplem4  46920  gpg3kgrtriexlem4  48185  gpg3kgrtriexlem6  48187  expnegico01  48618  eenglngeehlnmlem2  48838  inlinecirc02plem  48886