Theorem ltled 11382

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 11322	. . 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 11123   < clt 11267   ≤ cle 11268

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 2732  ax-sep 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398  ax-un 7736  ax-resscn 11181  ax-pre-lttri 11198

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 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  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 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-er 8696  df-en 8953  df-dom 8954  df-sdom 8955  df-pnf 11269  df-mnf 11270  df-xr 11271  df-ltxr 11272  df-le 11273

This theorem is used by:  ltnsymd  11383  mulge0  11756  msqge0  11759  addgt0d  11813  lt2addd  11861  lt2msq1  12123  uzwo3  12992  fznatpl1  13633  flflp1  13868  modaddmodup  13998  expmulnbnd  14299  fzsdom2  14493  repswcshw  14883  sgnmul  15180  isercolllem1  15752  caucvgrlem  15760  climcnds  15940  geomulcvg  15965  mertenslem1  15973  ruclem2  16320  ruclem12  16329  bitsfzo  16525  bitsmod  16526  nn0rppwr  16651  nn0expgcd  16654  lcmgcdlem  16696  isprm7  16799  4sqlem7  17036  vdwlem1  17073  chnub  18710  met1stc  24747  cfilucfil  24785  nlmvscnlem2  24911  icccmplem2  25050  reconnlem2  25054  xrhmeo  25174  cnheibor  25183  nmoleub2lem3  25343  ipcnlem2  25472  minveclem3b  25656  ivthlem1  25679  ivthlem2  25680  ivth2  25683  ivthle  25684  ivthle2  25685  ovollb2lem  25716  ovolicc2lem4  25748  ovolicc2lem5  25749  ioombl1lem4  25789  uniioombllem4  25814  uniioombllem5  25815  opnmbllem  25829  ismbf3d  25882  mbfi1fseqlem6  25948  itg2gt0  25988  dveflem  26206  dvferm1lem  26211  dvferm2lem  26213  rollelem  26216  rolle  26217  cmvth  26218  mvth  26219  c1liplem1  26223  dvgt0lem1  26229  dvivthlem1  26235  lhop1lem  26240  lhop1  26241  dvcnvrelem1  26244  dvcnvrelem2  26245  dvcvx  26247  dgradd2  26494  aaliou3lem8  26581  aaliou3lem7  26585  ulmdvlem1  26636  itgulm  26644  radcnvlt1  26654  radcnvle  26656  abelthlem7  26674  efcvx  26685  coseq0negpitopi  26741  tangtx  26743  tanabsge  26744  tanord  26775  abslogimle  26810  divlogrlim  26872  logno1  26873  logcnlem3  26881  logcnlem4  26882  logtayl  26897  logccv  26900  cxple  26932  rtprmirr  26997  chordthmlem4  27072  asinsin  27129  atanlogaddlem  27150  atantan  27160  cxp2limlem  27212  logdifbnd  27230  emcllem4  27235  harmonicbnd4  27247  lgamucov  27274  ftalem1  27309  ftalem2  27310  ftalem3  27311  basellem5  27321  basellem8  27324  chpchtsum  27455  bposlem1  27520  lgseisenlem1  27611  lgsquadlem1  27616  lgsquadlem2  27617  lgsquadlem3  27618  2sqreulem1  27682  2sqreunnlem1  27685  chebbnd1lem2  27706  chebbnd1lem3  27707  chtppilimlem1  27709  chto1ub  27712  chpo1ubb  27717  vmadivsumb  27719  dchrisumlem3  27727  mulog2sumlem1  27770  vmalogdivsum2  27774  vmalogdivsum  27775  2vmadivsumlem  27776  selbergb  27785  selberg2b  27788  chpdifbndlem1  27789  selberg3lem2  27794  selberg3  27795  selberg4lem1  27796  selberg4  27797  pntrsumbnd  27802  selberg3r  27805  selberg4r  27806  selberg34r  27807  pntrlog2bndlem1  27813  pntrlog2bndlem2  27814  pntrlog2bndlem3  27815  pntrlog2bndlem4  27816  pntrlog2bndlem5  27817  pntrlog2bndlem6a  27818  pntrlog2bndlem6  27819  pntrlog2bnd  27820  pntpbnd1a  27821  pntpbnd1  27822  pntpbnd2  27823  pntibndlem2  27827  pntlemb  27833  pntlemq  27837  pntlemr  27838  pntlemj  27839  pntlemf  27841  pntlemp  27846  ostth2lem2  27870  axpaschlem  29397  axlowdimlem16  29414  smcnlem  31178  bcm1n  33266  wrdt2ind  33395  cycpmco2lem6  33571  cyc3conja  33597  smatrcl  34306  fiunelros  34685  dya2icoseg  34788  eulerpartlemgc  34873  dstfrvunirn  34986  ballotlemfc0  35004  ballotlemfcc  35005  ballotlemimin  35017  ballotlemsgt1  35022  ballotlemfrcn0  35041  fdvposlt  35107  breprexp  35141  logdivsqrle  35158  hgt750leme  35166  tgoldbachgt  35171  lpadmax  35193  lpadright  35195  subfacval3  35768  erdszelem8  35777  cvmliftlem6  35869  cvmliftlem7  35870  cvmliftlem8  35871  cvmliftlem9  35872  cvmliftlem10  35873  sinccvglem  36251  dnibndlem9  37183  unbdqndv2lem2  37207  knoppndvlem14  37222  knoppndvlem18  37226  knoppndvlem19  37227  poimirlem7  38376  poimirlem15  38384  opnmbllem0  38405  itg2addnclem  38420  itg2addnclem3  38422  itg2addnc  38423  itg2gt0cn  38424  areacirclem1  38457  areacirc  38462  isbnd3  38534  cntotbnd  38546  rrnequiv  38585  lcmineqlem11  42905  lcmineqlem22  42916  3lexlogpow5ineq2  42921  3lexlogpow5ineq5  42926  dvrelogpow2b  42934  aks4d1p1p2  42936  aks4d1p1p4  42937  aks4d1p1p6  42939  aks4d1p1p7  42940  aks4d1p1p5  42941  aks4d1p1  42942  aks4d1p2  42943  aks4d1p3  42944  aks4d1p5  42946  aks4d1p7d1  42948  aks4d1p7  42949  aks4d1p8  42953  hashscontpow1  42987  aks6d1c2lem4  42993  aks6d1c5lem2  43004  sticksstones6  43017  sticksstones12a  43023  sticksstones12  43024  aks6d1c7lem1  43046  unitscyglem2  43062  posqsqznn  43211  redvmptabs  43235  readvrec  43237  fltnltalem  43508  irrapxlem3  43665  pellexlem2  43671  pellfundglb  43726  monotuz  43782  monotoddzzfi  43783  acongrep  43821  cvgdvgrat  45137  hashnzfz2  45145  hashnzfzclim  45146  binomcxplemnotnn0  45180  monoords  46130  xralrple2  46184  reclt0d  46216  reclt0  46220  uzublem  46258  cvgcaule  46319  iooiinicc  46372  iooiinioc  46386  limciccioolb  46451  limcicciooub  46465  lptre2pt  46468  limsupubuzlem  46540  limsup10exlem  46600  icccncfext  46715  cncfiooicclem1  46721  dvdivbd  46751  dvbdfbdioolem1  46756  dvbdfbdioolem2  46757  ioodvbdlimc1lem2  46760  ioodvbdlimc2lem  46762  dvnxpaek  46770  dvnmul  46771  volioc  46800  iblspltprt  46801  itgspltprt  46807  volico  46811  volioore  46818  voliooico  46820  voliccico  46827  stoweidlem1  46829  stoweidlem3  46831  stoweidlem7  46835  stoweidlem24  46852  stoweidlem26  46854  stoweidlem42  46870  wallispilem5  46897  stirlinglem1  46902  stirlinglem6  46907  stirlinglem7  46908  stirlinglem10  46911  stirlinglem12  46913  stirlinglem13  46914  stirlingr  46918  dirkertrigeqlem1  46926  fourierdlem10  46945  fourierdlem11  46946  fourierdlem12  46947  fourierdlem14  46949  fourierdlem15  46950  fourierdlem17  46952  fourierdlem19  46954  fourierdlem30  46965  fourierdlem37  46972  fourierdlem40  46975  fourierdlem41  46976  fourierdlem42  46977  fourierdlem47  46981  fourierdlem48  46982  fourierdlem49  46983  fourierdlem50  46984  fourierdlem51  46985  fourierdlem54  46988  fourierdlem63  46997  fourierdlem64  46998  fourierdlem65  46999  fourierdlem68  47002  fourierdlem73  47007  fourierdlem74  47008  fourierdlem76  47010  fourierdlem77  47011  fourierdlem78  47012  fourierdlem79  47013  fourierdlem81  47015  fourierdlem82  47016  fourierdlem83  47017  fourierdlem92  47026  fourierdlem93  47027  fourierdlem102  47036  fourierdlem103  47037  fourierdlem104  47038  fourierdlem107  47041  fourierdlem111  47045  fourierdlem114  47048  sqwvfoura  47056  sqwvfourb  47057  fouriersw  47059  etransclem19  47081  etransclem23  47085  etransclem35  47097  etransclem41  47103  qndenserrnbllem  47122  iundjiun  47288  carageniuncllem2  47350  caratheodorylem1  47354  hoicvr  47376  ovnsubaddlem1  47398  hsphoidmvle2  47413  hoidmv1lelem1  47419  hoidmv1lelem2  47420  hoidmvlelem1  47423  hoidmvlelem2  47424  hoidmvlelem3  47425  hoiqssbllem1  47450  hoiqssbllem2  47451  volico2  47469  iinhoiicclem  47501  iunhoiioolem  47503  vonioolem2  47509  vonicclem2  47512  pimdecfgtioo  47545  pimincfltioo  47546  smflimlem4  47602  smfmullem1  47619  smflimsuplem4  47651  gpg3kgrtriexlem4  49002  gpg3kgrtriexlem6  49004  expnegico01  49448  eenglngeehlnmlem2  49668  inlinecirc02plem  49716