Theorem ltled 11256

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

Syntax hints:   → wi 4   ∈ wcel 2111   class class class wbr 5086  ℝcr 11000   < clt 11141   ≤ cle 11142

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 5229  ax-nul 5239  ax-pow 5298  ax-pr 5365  ax-un 7663  ax-resscn 11058  ax-pre-lttri 11075

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 4279  df-if 4471  df-pw 4547  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4855  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5506  df-xp 5617  df-rel 5618  df-cnv 5619  df-co 5620  df-dm 5621  df-rn 5622  df-res 5623  df-ima 5624  df-iota 6432  df-fun 6478  df-fn 6479  df-f 6480  df-f1 6481  df-fo 6482  df-f1o 6483  df-fv 6484  df-er 8617  df-en 8865  df-dom 8866  df-sdom 8867  df-pnf 11143  df-mnf 11144  df-xr 11145  df-ltxr 11146  df-le 11147

This theorem is referenced by:  ltnsymd  11257  mulge0  11630  msqge0  11633  addgt0d  11687  lt2addd  11735  lt2msq1  12001  uzwo3  12836  fznatpl1  13473  flflp1  13706  modaddmodup  13836  expmulnbnd  14137  fzsdom2  14330  repswcshw  14714  isercolllem1  15567  caucvgrlem  15575  climcnds  15753  geomulcvg  15778  mertenslem1  15786  ruclem2  16136  ruclem12  16145  bitsfzo  16341  bitsmod  16342  nn0rppwr  16467  nn0expgcd  16470  lcmgcdlem  16512  isprm7  16614  4sqlem7  16851  vdwlem1  16888  chnub  18523  met1stc  24431  cfilucfil  24469  nlmvscnlem2  24595  icccmplem2  24734  reconnlem2  24738  xrhmeo  24866  cnheibor  24876  nmoleub2lem3  25037  ipcnlem2  25166  minveclem3b  25350  ivthlem1  25374  ivthlem2  25375  ivth2  25378  ivthle  25379  ivthle2  25380  ovollb2lem  25411  ovolicc2lem4  25443  ovolicc2lem5  25444  ioombl1lem4  25484  uniioombllem4  25509  uniioombllem5  25510  opnmbllem  25524  ismbf3d  25577  mbfi1fseqlem6  25643  itg2gt0  25683  dveflem  25905  dvferm1lem  25910  dvferm2lem  25912  rollelem  25915  rolle  25916  cmvth  25917  cmvthOLD  25918  mvth  25919  c1liplem1  25923  dvgt0lem1  25929  dvivthlem1  25935  lhop1lem  25940  lhop1  25941  dvcnvrelem1  25944  dvcnvrelem2  25945  dvcvx  25947  dgradd2  26196  aaliou3lem8  26275  aaliou3lem7  26279  ulmdvlem1  26331  itgulm  26339  radcnvlt1  26349  radcnvle  26351  abelthlem7  26370  efcvx  26381  coseq0negpitopi  26434  tangtx  26436  tanabsge  26437  tanord  26469  abslogimle  26504  divlogrlim  26566  logno1  26567  logcnlem3  26575  logcnlem4  26576  logtayl  26591  logccv  26594  cxple  26626  rtprmirr  26692  chordthmlem4  26767  asinsin  26824  atanlogaddlem  26845  atantan  26855  cxp2limlem  26908  logdifbnd  26926  emcllem4  26931  harmonicbnd4  26943  lgamucov  26970  ftalem1  27005  ftalem2  27006  ftalem3  27007  basellem5  27017  basellem8  27020  chpchtsum  27152  bposlem1  27217  lgseisenlem1  27308  lgsquadlem1  27313  lgsquadlem2  27314  lgsquadlem3  27315  2sqreulem1  27379  2sqreunnlem1  27382  chebbnd1lem2  27403  chebbnd1lem3  27404  chtppilimlem1  27406  chto1ub  27409  chpo1ubb  27414  vmadivsumb  27416  dchrisumlem3  27424  mulog2sumlem1  27467  vmalogdivsum2  27471  vmalogdivsum  27472  2vmadivsumlem  27473  selbergb  27482  selberg2b  27485  chpdifbndlem1  27486  selberg3lem2  27491  selberg3  27492  selberg4lem1  27493  selberg4  27494  pntrsumbnd  27499  selberg3r  27502  selberg4r  27503  selberg34r  27504  pntrlog2bndlem1  27510  pntrlog2bndlem2  27511  pntrlog2bndlem3  27512  pntrlog2bndlem4  27513  pntrlog2bndlem5  27514  pntrlog2bndlem6a  27515  pntrlog2bndlem6  27516  pntrlog2bnd  27517  pntpbnd1a  27518  pntpbnd1  27519  pntpbnd2  27520  pntibndlem2  27524  pntlemb  27530  pntlemq  27534  pntlemr  27535  pntlemj  27536  pntlemf  27538  pntlemp  27543  ostth2lem2  27567  axpaschlem  28913  axlowdimlem16  28930  smcnlem  30669  bcm1n  32769  sgnmul  32810  wrdt2ind  32926  cycpmco2lem6  33092  cyc3conja  33118  smatrcl  33801  fiunelros  34179  dya2icoseg  34282  eulerpartlemgc  34367  dstfrvunirn  34480  ballotlemfc0  34498  ballotlemfcc  34499  ballotlemimin  34511  ballotlemsgt1  34516  ballotlemfrcn0  34535  fdvposlt  34604  breprexp  34638  logdivsqrle  34655  hgt750leme  34663  tgoldbachgt  34668  lpadmax  34687  lpadright  34689  subfacval3  35225  erdszelem8  35234  cvmliftlem6  35326  cvmliftlem7  35327  cvmliftlem8  35328  cvmliftlem9  35329  cvmliftlem10  35330  sinccvglem  35708  dnibndlem9  36520  unbdqndv2lem2  36544  knoppndvlem14  36559  knoppndvlem18  36563  knoppndvlem19  36564  poimirlem7  37667  poimirlem15  37675  opnmbllem0  37696  itg2addnclem  37711  itg2addnclem3  37713  itg2addnc  37714  itg2gt0cn  37715  areacirclem1  37748  areacirc  37753  isbnd3  37824  cntotbnd  37836  rrnequiv  37875  lcmineqlem11  42072  lcmineqlem22  42083  3lexlogpow5ineq2  42088  3lexlogpow5ineq5  42093  dvrelogpow2b  42101  aks4d1p1p2  42103  aks4d1p1p4  42104  aks4d1p1p6  42106  aks4d1p1p7  42107  aks4d1p1p5  42108  aks4d1p1  42109  aks4d1p2  42110  aks4d1p3  42111  aks4d1p5  42113  aks4d1p7d1  42115  aks4d1p7  42116  aks4d1p8  42120  hashscontpow1  42154  aks6d1c2lem4  42160  aks6d1c5lem2  42171  sticksstones6  42184  sticksstones12a  42190  sticksstones12  42191  aks6d1c7lem1  42213  unitscyglem2  42229  posqsqznn  42369  redvmptabs  42393  readvrec  42395  fltnltalem  42695  irrapxlem3  42857  pellexlem2  42863  pellfundglb  42918  monotuz  42974  monotoddzzfi  42975  acongrep  43013  cvgdvgrat  44346  hashnzfz2  44354  hashnzfzclim  44355  binomcxplemnotnn0  44389  monoords  45338  xralrple2  45393  reclt0d  45425  reclt0  45429  uzublem  45468  cvgcaule  45529  iooiinicc  45582  iooiinioc  45596  limciccioolb  45661  limcicciooub  45675  lptre2pt  45678  limsupubuzlem  45750  limsup10exlem  45810  icccncfext  45925  cncfiooicclem1  45931  dvdivbd  45961  dvbdfbdioolem1  45966  dvbdfbdioolem2  45967  ioodvbdlimc1lem2  45970  ioodvbdlimc2lem  45972  dvnxpaek  45980  dvnmul  45981  volioc  46010  iblspltprt  46011  itgspltprt  46017  volico  46021  volioore  46028  voliooico  46030  voliccico  46037  stoweidlem1  46039  stoweidlem3  46041  stoweidlem7  46045  stoweidlem24  46062  stoweidlem26  46064  stoweidlem42  46080  wallispilem5  46107  stirlinglem1  46112  stirlinglem6  46117  stirlinglem7  46118  stirlinglem10  46121  stirlinglem12  46123  stirlinglem13  46124  stirlingr  46128  dirkertrigeqlem1  46136  fourierdlem10  46155  fourierdlem11  46156  fourierdlem12  46157  fourierdlem14  46159  fourierdlem15  46160  fourierdlem17  46162  fourierdlem19  46164  fourierdlem30  46175  fourierdlem37  46182  fourierdlem40  46185  fourierdlem41  46186  fourierdlem42  46187  fourierdlem47  46191  fourierdlem48  46192  fourierdlem49  46193  fourierdlem50  46194  fourierdlem51  46195  fourierdlem54  46198  fourierdlem63  46207  fourierdlem64  46208  fourierdlem65  46209  fourierdlem68  46212  fourierdlem73  46217  fourierdlem74  46218  fourierdlem76  46220  fourierdlem77  46221  fourierdlem78  46222  fourierdlem79  46223  fourierdlem81  46225  fourierdlem82  46226  fourierdlem83  46227  fourierdlem92  46236  fourierdlem93  46237  fourierdlem102  46246  fourierdlem103  46247  fourierdlem104  46248  fourierdlem107  46251  fourierdlem111  46255  fourierdlem114  46258  sqwvfoura  46266  sqwvfourb  46267  fouriersw  46269  etransclem19  46291  etransclem23  46295  etransclem35  46307  etransclem41  46313  qndenserrnbllem  46332  iundjiun  46498  carageniuncllem2  46560  caratheodorylem1  46564  hoicvr  46586  ovnsubaddlem1  46608  hsphoidmvle2  46623  hoidmv1lelem1  46629  hoidmv1lelem2  46630  hoidmvlelem1  46633  hoidmvlelem2  46634  hoidmvlelem3  46635  hoiqssbllem1  46660  hoiqssbllem2  46661  volico2  46679  iinhoiicclem  46711  iunhoiioolem  46713  vonioolem2  46719  vonicclem2  46722  pimdecfgtioo  46755  pimincfltioo  46756  smflimlem4  46812  smfmullem1  46829  smflimsuplem4  46861  gpg3kgrtriexlem4  48117  gpg3kgrtriexlem6  48119  expnegico01  48550  eenglngeehlnmlem2  48770  inlinecirc02plem  48818