Theorem ltled 10064

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

Syntax hints:   → wi 4   ∈ wcel 1977   class class class wbr 4583  ℝcr 9814   < clt 9953   ≤ cle 9954

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-resscn 9872  ax-pre-lttri 9889

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-er 7629  df-en 7842  df-dom 7843  df-sdom 7844  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959

This theorem is referenced by:  ltnsymd  10065  mulge0  10425  msqge0  10428  addgt0d  10481  lt2addd  10529  lt2msq1  10786  uzwo3  11659  fznatpl1  12265  flflp1  12470  modaddmodup  12595  expmulnbnd  12858  fzsdom2  13075  repswcshw  13409  isercolllem1  14243  caucvgrlem  14251  climcnds  14422  geomulcvg  14446  mertenslem1  14455  ruclem2  14800  ruclem12  14809  bitsfzo  14995  bitsmod  14996  lcmgcdlem  15157  isprm7  15258  4sqlem7  15486  vdwlem1  15523  met1stc  22136  cfilucfil  22174  nlmvscnlem2  22299  icccmplem2  22434  reconnlem2  22438  xrhmeo  22553  cnheibor  22562  nmoleub2lem3  22723  ipcnlem2  22851  minveclem3b  23007  ivthlem1  23027  ivthlem2  23028  ivth2  23031  ivthle  23032  ivthle2  23033  ovollb2lem  23063  ovolicc2lem4  23095  ovolicc2lem5  23096  ioombl1lem4  23136  uniioombllem4  23160  uniioombllem5  23161  opnmbllem  23175  ismbf3d  23227  mbfi1fseqlem6  23293  itg2gt0  23333  dveflem  23546  dvferm1lem  23551  dvferm2lem  23553  rollelem  23556  rolle  23557  cmvth  23558  mvth  23559  c1liplem1  23563  dvgt0lem1  23569  dvivthlem1  23575  lhop1lem  23580  lhop1  23581  dvcnvrelem1  23584  dvcnvrelem2  23585  dvcvx  23587  dgradd2  23828  aaliou3lem8  23904  aaliou3lem7  23908  ulmdvlem1  23958  itgulm  23966  radcnvlt1  23976  radcnvle  23978  abelthlem7  23996  efcvx  24007  coseq0negpitopi  24059  tangtx  24061  tanabsge  24062  tanord  24088  abslogimle  24124  divlogrlim  24181  logno1  24182  logcnlem3  24190  logcnlem4  24191  logtayl  24206  logccv  24209  cxple  24241  chordthmlem4  24362  asinsin  24419  atanlogaddlem  24440  atantan  24450  cxp2limlem  24502  logdifbnd  24520  emcllem4  24525  harmonicbnd4  24537  lgamucov  24564  ftalem1  24599  ftalem2  24600  ftalem3  24601  basellem5  24611  basellem8  24614  chpchtsum  24744  bposlem1  24809  lgseisenlem1  24900  lgsquadlem1  24905  lgsquadlem2  24906  lgsquadlem3  24907  chebbnd1lem2  24959  chebbnd1lem3  24960  chtppilimlem1  24962  chto1ub  24965  chpo1ubb  24970  vmadivsumb  24972  dchrisumlem3  24980  mulog2sumlem1  25023  vmalogdivsum2  25027  vmalogdivsum  25028  2vmadivsumlem  25029  selbergb  25038  selberg2b  25041  chpdifbndlem1  25042  selberg3lem2  25047  selberg3  25048  selberg4lem1  25049  selberg4  25050  pntrsumbnd  25055  selberg3r  25058  selberg4r  25059  selberg34r  25060  pntrlog2bndlem1  25066  pntrlog2bndlem2  25067  pntrlog2bndlem3  25068  pntrlog2bndlem4  25069  pntrlog2bndlem5  25070  pntrlog2bndlem6a  25071  pntrlog2bndlem6  25072  pntrlog2bnd  25073  pntpbnd1a  25074  pntpbnd1  25075  pntpbnd2  25076  pntibndlem2  25080  pntlemb  25086  pntlemq  25090  pntlemr  25091  pntlemj  25092  pntlemf  25094  pntlemp  25099  ostth2lem2  25123  axpaschlem  25620  axlowdimlem16  25637  smcnlem  26936  bcm1n  28941  smatrcl  29190  fiunelros  29564  dya2icoseg  29666  eulerpartlemgc  29751  dstfrvunirn  29863  ballotlemfc0  29881  ballotlemfcc  29882  ballotlemimin  29894  ballotlemsgt1  29899  ballotlemfrcn0  29918  sgnmul  29931  subfacval3  30425  erdszelem8  30434  cvmliftlem6  30526  cvmliftlem7  30527  cvmliftlem8  30528  cvmliftlem9  30529  cvmliftlem10  30530  sinccvglem  30820  dnibndlem9  31646  unbdqndv2lem2  31671  knoppndvlem14  31686  knoppndvlem18  31690  knoppndvlem19  31691  poimirlem7  32586  poimirlem15  32594  opnmbllem0  32615  itg2addnclem  32631  itg2addnclem3  32633  itg2addnc  32634  itg2gt0cn  32635  areacirclem1  32670  areacirc  32675  isbnd3  32753  cntotbnd  32765  rrnequiv  32804  irrapxlem3  36406  pellexlem2  36412  pellfundglb  36467  monotuz  36524  monotoddzzfi  36525  acongrep  36565  cvgdvgrat  37534  hashnzfz2  37542  hashnzfzclim  37543  binomcxplemnotnn0  37577  monoords  38452  xralrple2  38511  reclt0d  38548  reclt0  38555  iooiinicc  38616  iooiinioc  38630  limciccioolb  38688  limcicciooub  38704  lptre2pt  38707  icccncfext  38773  cncfiooicclem1  38779  dvdivbd  38813  dvbdfbdioolem1  38818  dvbdfbdioolem2  38819  ioodvbdlimc1lem2  38822  ioodvbdlimc2lem  38824  dvnxpaek  38832  dvnmul  38833  volioc  38864  iblspltprt  38865  itgspltprt  38871  volico  38876  volioore  38883  voliooico  38885  voliccico  38892  stoweidlem1  38894  stoweidlem3  38896  stoweidlem7  38900  stoweidlem24  38917  stoweidlem26  38919  stoweidlem42  38935  wallispilem5  38962  stirlinglem1  38967  stirlinglem6  38972  stirlinglem7  38973  stirlinglem10  38976  stirlinglem12  38978  stirlinglem13  38979  stirlingr  38983  dirkertrigeqlem1  38991  fourierdlem10  39010  fourierdlem11  39011  fourierdlem12  39012  fourierdlem14  39014  fourierdlem15  39015  fourierdlem17  39017  fourierdlem19  39019  fourierdlem30  39030  fourierdlem37  39037  fourierdlem40  39040  fourierdlem41  39041  fourierdlem42  39042  fourierdlem47  39046  fourierdlem48  39047  fourierdlem49  39048  fourierdlem50  39049  fourierdlem51  39050  fourierdlem54  39053  fourierdlem63  39062  fourierdlem64  39063  fourierdlem65  39064  fourierdlem68  39067  fourierdlem73  39072  fourierdlem74  39073  fourierdlem76  39075  fourierdlem77  39076  fourierdlem78  39077  fourierdlem79  39078  fourierdlem81  39080  fourierdlem82  39081  fourierdlem83  39082  fourierdlem92  39091  fourierdlem93  39092  fourierdlem102  39101  fourierdlem103  39102  fourierdlem104  39103  fourierdlem107  39106  fourierdlem111  39110  fourierdlem114  39113  sqwvfoura  39121  sqwvfourb  39122  fouriersw  39124  etransclem19  39146  etransclem23  39150  etransclem35  39162  etransclem41  39168  qndenserrnbllem  39190  iundjiun  39353  carageniuncllem2  39412  caratheodorylem1  39416  hoicvr  39438  ovnsubaddlem1  39460  hsphoidmvle2  39475  hoidmv1lelem1  39481  hoidmv1lelem2  39482  hoidmvlelem1  39485  hoidmvlelem2  39486  hoidmvlelem3  39487  hoiqssbllem1  39512  hoiqssbllem2  39513  volico2  39531  iinhoiicclem  39564  iunhoiioolem  39566  vonioolem2  39572  vonicclem2  39575  pimdecfgtioo  39604  pimincfltioo  39605  smflimlem4  39660  smfmullem1  39676  expnegico01  42102