Theorem ltled 11451

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   class class class wbr 5103  ℝcr 11192   < clt 11336   ≤ cle 11337

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7749  ax-resscn 11250  ax-pre-lttri 11267

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-er 8710  df-en 8967  df-dom 8968  df-sdom 8969  df-pnf 11338  df-mnf 11339  df-xr 11340  df-ltxr 11341  df-le 11342

This theorem is used by:  ltnsymd  11452  mulge0  11827  msqge0  11830  addgt0d  11884  lt2addd  11932  lt2msq1  12194  uzwo3  13063  fznatpl1  13705  flflp1  13940  modaddmodup  14070  expmulnbnd  14372  fzsdom2  14566  repswcshw  14956  sgnmul  15253  isercolllem1  15825  caucvgrlem  15833  climcnds  16013  geomulcvg  16038  mertenslem1  16046  ruclem2  16393  ruclem12  16402  bitsfzo  16598  bitsmod  16599  nn0rppwr  16728  nn0expgcd  16731  lcmgcdlem  16774  isprm7  16877  posqsqznn  16929  4sqlem7  17115  vdwlem1  17152  chnub  18789  met1stc  24833  cfilucfil  24871  nlmvscnlem2  24997  icccmplem2  25136  reconnlem2  25140  xrhmeo  25260  cnheibor  25269  nmoleub2lem3  25429  ipcnlem2  25558  minveclem3b  25742  ivthlem1  25765  ivthlem2  25766  ivth2  25769  ivthle  25770  ivthle2  25771  ovollb2lem  25802  ovolicc2lem4  25834  ovolicc2lem5  25835  ioombl1lem4  25875  uniioombllem4  25900  uniioombllem5  25901  opnmbllem  25915  ismbf3d  25968  mbfi1fseqlem6  26034  itg2gt0  26074  dveflem  26292  dvferm1lem  26297  dvferm2lem  26299  rollelem  26302  rolle  26303  cmvth  26304  mvth  26305  c1liplem1  26309  dvgt0lem1  26315  dvivthlem1  26321  lhop1lem  26326  lhop1  26327  dvcnvrelem1  26330  dvcnvrelem2  26331  dvcvx  26333  dgradd2  26580  aaliou3lem8  26665  aaliou3lem7  26669  ulmdvlem1  26720  itgulm  26728  radcnvlt1  26738  radcnvle  26740  abelthlem7  26758  efcvx  26769  coseq0negpitopi  26825  tangtx  26827  tanabsge  26828  tanord  26859  abslogimle  26894  divlogrlim  26956  logno1  26957  logcnlem3  26965  logcnlem4  26966  logtayl  26981  logccv  26984  cxple  27016  rtprmirr  27081  chordthmlem4  27156  asinsin  27213  atanlogaddlem  27234  atantan  27244  cxp2limlem  27296  logdifbnd  27314  emcllem4  27319  harmonicbnd4  27331  lgamucov  27358  ftalem1  27393  ftalem2  27394  ftalem3  27395  basellem5  27405  basellem8  27408  chpchtsum  27539  bposlem1  27604  lgseisenlem1  27695  lgsquadlem1  27700  lgsquadlem2  27701  lgsquadlem3  27702  2sqreulem1  27766  2sqreunnlem1  27769  chebbnd1lem2  27790  chebbnd1lem3  27791  chtppilimlem1  27793  chto1ub  27796  chpo1ubb  27801  vmadivsumb  27803  dchrisumlem3  27811  mulog2sumlem1  27854  vmalogdivsum2  27858  vmalogdivsum  27859  2vmadivsumlem  27860  selbergb  27869  selberg2b  27872  chpdifbndlem1  27873  selberg3lem2  27878  selberg3  27879  selberg4lem1  27880  selberg4  27881  pntrsumbnd  27886  selberg3r  27889  selberg4r  27890  selberg34r  27891  pntrlog2bndlem1  27897  pntrlog2bndlem2  27898  pntrlog2bndlem3  27899  pntrlog2bndlem4  27900  pntrlog2bndlem5  27901  pntrlog2bndlem6a  27902  pntrlog2bndlem6  27903  pntrlog2bnd  27904  pntpbnd1a  27905  pntpbnd1  27906  pntpbnd2  27907  pntibndlem2  27911  pntlemb  27917  pntlemq  27921  pntlemr  27922  pntlemj  27923  pntlemf  27925  pntlemp  27930  ostth2lem2  27954  axpaschlem  29511  axlowdimlem16  29528  smcnlem  31292  bcm1n  33380  wrdt2ind  33509  cycpmco2lem6  33685  cyc3conja  33711  smatrcl  34421  fiunelros  34800  dya2icoseg  34902  eulerpartlemgc  34987  dstfrvunirn  35100  ballotlemfc0  35118  ballotlemfcc  35119  ballotlemimin  35131  ballotlemsgt1  35136  ballotlemfrcn0  35155  fdvposlt  35221  breprexp  35255  logdivsqrle  35272  hgt750leme  35280  tgoldbachgt  35285  lpadmax  35307  lpadright  35309  subfacval3  35933  erdszelem8  35942  cvmliftlem6  36034  cvmliftlem7  36035  cvmliftlem8  36036  cvmliftlem9  36037  cvmliftlem10  36038  sinccvglem  36416  dnibndlem9  37332  unbdqndv2lem2  37356  knoppndvlem14  37371  knoppndvlem18  37375  knoppndvlem19  37376  poimirlem7  38525  poimirlem15  38533  opnmbllem0  38554  itg2addnclem  38569  itg2addnclem3  38571  itg2addnc  38572  itg2gt0cn  38573  areacirclem1  38606  areacirc  38611  isbnd3  38698  cntotbnd  38710  rrnequiv  38749  lcmineqlem11  43069  lcmineqlem22  43080  3lexlogpow5ineq2  43085  3lexlogpow5ineq5  43090  dvrelogpow2b  43098  aks4d1p1p2  43100  aks4d1p1p4  43101  aks4d1p1p6  43103  aks4d1p1p7  43104  aks4d1p1p5  43105  aks4d1p1  43106  aks4d1p2  43107  aks4d1p3  43108  aks4d1p5  43110  aks4d1p7d1  43112  aks4d1p7  43113  aks4d1p8  43117  hashscontpow1  43151  aks6d1c2lem4  43157  aks6d1c5lem2  43168  sticksstones6  43181  sticksstones12a  43187  sticksstones12  43188  aks6d1c7lem1  43210  unitscyglem2  43226  redvmptabs  43391  readvrec  43393  fltnltalem  43653  irrapxlem3  43810  pellexlem2  43816  pellfundglb  43871  monotuz  43927  monotoddzzfi  43928  acongrep  43966  cvgdvgrat  45282  hashnzfz2  45290  hashnzfzclim  45291  binomcxplemnotnn0  45325  monoords  46282  xralrple2  46335  reclt0d  46367  reclt0  46371  uzublem  46409  cvgcaule  46470  iooiinicc  46523  iooiinioc  46537  limciccioolb  46602  limcicciooub  46616  lptre2pt  46619  limsupubuzlem  46691  limsup10exlem  46751  icccncfext  46866  cncfiooicclem1  46872  dvdivbd  46902  dvbdfbdioolem1  46907  dvbdfbdioolem2  46908  ioodvbdlimc1lem2  46911  ioodvbdlimc2lem  46913  dvnxpaek  46921  dvnmul  46922  volioc  46951  iblspltprt  46952  itgspltprt  46958  volico  46962  volioore  46969  voliooico  46971  voliccico  46978  stoweidlem1  46980  stoweidlem3  46982  stoweidlem7  46986  stoweidlem24  47003  stoweidlem26  47005  stoweidlem42  47021  wallispilem5  47048  stirlinglem1  47053  stirlinglem6  47058  stirlinglem7  47059  stirlinglem10  47062  stirlinglem12  47064  stirlinglem13  47065  stirlingr  47069  dirkertrigeqlem1  47077  fourierdlem10  47096  fourierdlem11  47097  fourierdlem12  47098  fourierdlem14  47100  fourierdlem15  47101  fourierdlem17  47103  fourierdlem19  47105  fourierdlem30  47116  fourierdlem37  47123  fourierdlem40  47126  fourierdlem41  47127  fourierdlem42  47128  fourierdlem47  47132  fourierdlem48  47133  fourierdlem49  47134  fourierdlem50  47135  fourierdlem51  47136  fourierdlem54  47139  fourierdlem63  47148  fourierdlem64  47149  fourierdlem65  47150  fourierdlem68  47153  fourierdlem73  47158  fourierdlem74  47159  fourierdlem76  47161  fourierdlem77  47162  fourierdlem78  47163  fourierdlem79  47164  fourierdlem81  47166  fourierdlem82  47167  fourierdlem83  47168  fourierdlem92  47177  fourierdlem93  47178  fourierdlem102  47187  fourierdlem103  47188  fourierdlem104  47189  fourierdlem107  47192  fourierdlem111  47196  fourierdlem114  47199  sqwvfoura  47207  sqwvfourb  47208  fouriersw  47210  etransclem19  47232  etransclem23  47236  etransclem35  47248  etransclem41  47254  qndenserrnbllem  47273  iundjiun  47439  carageniuncllem2  47501  caratheodorylem1  47505  hoicvr  47527  ovnsubaddlem1  47549  hsphoidmvle2  47564  hoidmv1lelem1  47570  hoidmv1lelem2  47571  hoidmvlelem1  47574  hoidmvlelem2  47575  hoidmvlelem3  47576  hoiqssbllem1  47601  hoiqssbllem2  47602  volico2  47620  iinhoiicclem  47652  iunhoiioolem  47654  vonioolem2  47660  vonicclem2  47663  pimdecfgtioo  47696  pimincfltioo  47697  smflimlem4  47753  smfmullem1  47770  smflimsuplem4  47802  gpg3kgrtriexlem4  49153  gpg3kgrtriexlem6  49155  expnegico01  49599  eenglngeehlnmlem2  49819  inlinecirc02plem  49867