Theorem ltled 11364

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2142   class class class wbr 5108  ℝcr 11105   < clt 11249   ≤ cle 11250

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5256  ax-nul 5268  ax-pow 5335  ax-pr 5403  ax-un 7734  ax-resscn 11163  ax-pre-lttri 11180

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-nf 1813  df-sb 2096  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3064  df-ral 3079  df-rex 3089  df-rab 3416  df-v 3456  df-sbc 3744  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4487  df-pw 4563  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-br 5109  df-opab 5173  df-mpt 5192  df-id 5555  df-xp 5666  df-rel 5667  df-cnv 5668  df-co 5669  df-dm 5670  df-rn 5671  df-res 5672  df-ima 5673  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-er 8692  df-en 8942  df-dom 8943  df-sdom 8944  df-pnf 11251  df-mnf 11252  df-xr 11253  df-ltxr 11254  df-le 11255

This theorem is used by:  ltnsymd  11365  mulge0  11738  msqge0  11741  addgt0d  11795  lt2addd  11843  lt2msq1  12105  uzwo3  12973  fznatpl1  13613  flflp1  13847  modaddmodup  13977  expmulnbnd  14278  fzsdom2  14472  repswcshw  14856  sgnmul  15151  isercolllem1  15723  caucvgrlem  15731  climcnds  15912  geomulcvg  15937  mertenslem1  15945  ruclem2  16294  ruclem12  16303  bitsfzo  16499  bitsmod  16500  nn0rppwr  16625  nn0expgcd  16628  lcmgcdlem  16670  isprm7  16773  4sqlem7  17010  vdwlem1  17047  chnub  18684  met1stc  24689  cfilucfil  24727  nlmvscnlem2  24853  icccmplem2  24992  reconnlem2  24996  xrhmeo  25116  cnheibor  25125  nmoleub2lem3  25285  ipcnlem2  25414  minveclem3b  25598  ivthlem1  25621  ivthlem2  25622  ivth2  25625  ivthle  25626  ivthle2  25627  ovollb2lem  25658  ovolicc2lem4  25690  ovolicc2lem5  25691  ioombl1lem4  25731  uniioombllem4  25756  uniioombllem5  25757  opnmbllem  25771  ismbf3d  25824  mbfi1fseqlem6  25890  itg2gt0  25930  dveflem  26149  dvferm1lem  26154  dvferm2lem  26156  rollelem  26159  rolle  26160  cmvth  26161  mvth  26162  c1liplem1  26166  dvgt0lem1  26172  dvivthlem1  26178  lhop1lem  26183  lhop1  26184  dvcnvrelem1  26187  dvcnvrelem2  26188  dvcvx  26190  dgradd2  26436  aaliou3lem8  26519  aaliou3lem7  26523  ulmdvlem1  26574  itgulm  26582  radcnvlt1  26592  radcnvle  26594  abelthlem7  26612  efcvx  26623  coseq0negpitopi  26679  tangtx  26681  tanabsge  26682  tanord  26714  abslogimle  26749  divlogrlim  26811  logno1  26812  logcnlem3  26820  logcnlem4  26821  logtayl  26836  logccv  26839  cxple  26871  rtprmirr  26936  chordthmlem4  27011  asinsin  27068  atanlogaddlem  27089  atantan  27099  cxp2limlem  27151  logdifbnd  27169  emcllem4  27174  harmonicbnd4  27186  lgamucov  27213  ftalem1  27248  ftalem2  27249  ftalem3  27250  basellem5  27260  basellem8  27263  chpchtsum  27394  bposlem1  27459  lgseisenlem1  27550  lgsquadlem1  27555  lgsquadlem2  27556  lgsquadlem3  27557  2sqreulem1  27621  2sqreunnlem1  27624  chebbnd1lem2  27645  chebbnd1lem3  27646  chtppilimlem1  27648  chto1ub  27651  chpo1ubb  27656  vmadivsumb  27658  dchrisumlem3  27666  mulog2sumlem1  27709  vmalogdivsum2  27713  vmalogdivsum  27714  2vmadivsumlem  27715  selbergb  27724  selberg2b  27727  chpdifbndlem1  27728  selberg3lem2  27733  selberg3  27734  selberg4lem1  27735  selberg4  27736  pntrsumbnd  27741  selberg3r  27744  selberg4r  27745  selberg34r  27746  pntrlog2bndlem1  27752  pntrlog2bndlem2  27753  pntrlog2bndlem3  27754  pntrlog2bndlem4  27755  pntrlog2bndlem5  27756  pntrlog2bndlem6a  27757  pntrlog2bndlem6  27758  pntrlog2bnd  27759  pntpbnd1a  27760  pntpbnd1  27761  pntpbnd2  27762  pntibndlem2  27766  pntlemb  27772  pntlemq  27776  pntlemr  27777  pntlemj  27778  pntlemf  27780  pntlemp  27785  ostth2lem2  27809  axpaschlem  29301  axlowdimlem16  29318  smcnlem  31060  bcm1n  33151  wrdt2ind  33282  cycpmco2lem6  33460  cyc3conja  33486  smatrcl  34195  fiunelros  34573  dya2icoseg  34676  eulerpartlemgc  34761  dstfrvunirn  34874  ballotlemfc0  34892  ballotlemfcc  34893  ballotlemimin  34905  ballotlemsgt1  34910  ballotlemfrcn0  34929  fdvposlt  34995  breprexp  35029  logdivsqrle  35046  hgt750leme  35054  tgoldbachgt  35059  lpadmax  35081  lpadright  35083  subfacval3  35689  erdszelem8  35698  cvmliftlem6  35790  cvmliftlem7  35791  cvmliftlem8  35792  cvmliftlem9  35793  cvmliftlem10  35794  sinccvglem  36172  dnibndlem9  37103  unbdqndv2lem2  37127  knoppndvlem14  37142  knoppndvlem18  37146  knoppndvlem19  37147  poimirlem7  38306  poimirlem15  38314  opnmbllem0  38335  itg2addnclem  38350  itg2addnclem3  38352  itg2addnc  38353  itg2gt0cn  38354  areacirclem1  38387  areacirc  38392  isbnd3  38463  cntotbnd  38475  rrnequiv  38514  lcmineqlem11  42834  lcmineqlem22  42845  3lexlogpow5ineq2  42850  3lexlogpow5ineq5  42855  dvrelogpow2b  42863  aks4d1p1p2  42865  aks4d1p1p4  42866  aks4d1p1p6  42868  aks4d1p1p7  42869  aks4d1p1p5  42870  aks4d1p1  42871  aks4d1p2  42872  aks4d1p3  42873  aks4d1p5  42875  aks4d1p7d1  42877  aks4d1p7  42878  aks4d1p8  42882  hashscontpow1  42916  aks6d1c2lem4  42922  aks6d1c5lem2  42933  sticksstones6  42946  sticksstones12a  42952  sticksstones12  42953  aks6d1c7lem1  42975  unitscyglem2  42991  posqsqznn  43125  redvmptabs  43149  readvrec  43151  fltnltalem  43422  irrapxlem3  43579  pellexlem2  43585  pellfundglb  43640  monotuz  43696  monotoddzzfi  43697  acongrep  43735  cvgdvgrat  45051  hashnzfz2  45059  hashnzfzclim  45060  binomcxplemnotnn0  45094  monoords  46044  xralrple2  46098  reclt0d  46130  reclt0  46134  uzublem  46172  cvgcaule  46233  iooiinicc  46286  iooiinioc  46300  limciccioolb  46365  limcicciooub  46379  lptre2pt  46382  limsupubuzlem  46454  limsup10exlem  46514  icccncfext  46629  cncfiooicclem1  46635  dvdivbd  46665  dvbdfbdioolem1  46670  dvbdfbdioolem2  46671  ioodvbdlimc1lem2  46674  ioodvbdlimc2lem  46676  dvnxpaek  46684  dvnmul  46685  volioc  46714  iblspltprt  46715  itgspltprt  46721  volico  46725  volioore  46732  voliooico  46734  voliccico  46741  stoweidlem1  46743  stoweidlem3  46745  stoweidlem7  46749  stoweidlem24  46766  stoweidlem26  46768  stoweidlem42  46784  wallispilem5  46811  stirlinglem1  46816  stirlinglem6  46821  stirlinglem7  46822  stirlinglem10  46825  stirlinglem12  46827  stirlinglem13  46828  stirlingr  46832  dirkertrigeqlem1  46840  fourierdlem10  46859  fourierdlem11  46860  fourierdlem12  46861  fourierdlem14  46863  fourierdlem15  46864  fourierdlem17  46866  fourierdlem19  46868  fourierdlem30  46879  fourierdlem37  46886  fourierdlem40  46889  fourierdlem41  46890  fourierdlem42  46891  fourierdlem47  46895  fourierdlem48  46896  fourierdlem49  46897  fourierdlem50  46898  fourierdlem51  46899  fourierdlem54  46902  fourierdlem63  46911  fourierdlem64  46912  fourierdlem65  46913  fourierdlem68  46916  fourierdlem73  46921  fourierdlem74  46922  fourierdlem76  46924  fourierdlem77  46925  fourierdlem78  46926  fourierdlem79  46927  fourierdlem81  46929  fourierdlem82  46930  fourierdlem83  46931  fourierdlem92  46940  fourierdlem93  46941  fourierdlem102  46950  fourierdlem103  46951  fourierdlem104  46952  fourierdlem107  46955  fourierdlem111  46959  fourierdlem114  46962  sqwvfoura  46970  sqwvfourb  46971  fouriersw  46973  etransclem19  46995  etransclem23  46999  etransclem35  47011  etransclem41  47017  qndenserrnbllem  47036  iundjiun  47202  carageniuncllem2  47264  caratheodorylem1  47268  hoicvr  47290  ovnsubaddlem1  47312  hsphoidmvle2  47327  hoidmv1lelem1  47333  hoidmv1lelem2  47334  hoidmvlelem1  47337  hoidmvlelem2  47338  hoidmvlelem3  47339  hoiqssbllem1  47364  hoiqssbllem2  47365  volico2  47383  iinhoiicclem  47415  iunhoiioolem  47417  vonioolem2  47423  vonicclem2  47426  pimdecfgtioo  47459  pimincfltioo  47460  smflimlem4  47516  smfmullem1  47533  smflimsuplem4  47565  gpg3kgrtriexlem4  48879  gpg3kgrtriexlem6  48881  expnegico01  49326  eenglngeehlnmlem2  49546  inlinecirc02plem  49594