Theorem ltled 11354

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

Syntax hints:   → wi 4   ∈ wcel 2149   class class class wbr 5110  ℝcr 11095   < clt 11239   ≤ cle 11240

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5258  ax-nul 5268  ax-pow 5334  ax-pr 5402  ax-un 7730  ax-resscn 11153  ax-pre-lttri 11170

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-nel 3071  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6490  df-fun 6536  df-fn 6537  df-f 6538  df-f1 6539  df-fo 6540  df-f1o 6541  df-fv 6542  df-er 8690  df-en 8940  df-dom 8941  df-sdom 8942  df-pnf 11241  df-mnf 11242  df-xr 11243  df-ltxr 11244  df-le 11245

This theorem is referenced by:  ltnsymd  11355  mulge0  11728  msqge0  11731  addgt0d  11785  lt2addd  11833  lt2msq1  12095  uzwo3  12963  fznatpl1  13602  flflp1  13836  modaddmodup  13966  expmulnbnd  14267  fzsdom2  14461  repswcshw  14845  sgnmul  15140  isercolllem1  15712  caucvgrlem  15720  climcnds  15901  geomulcvg  15926  mertenslem1  15934  ruclem2  16284  ruclem12  16293  bitsfzo  16489  bitsmod  16490  nn0rppwr  16615  nn0expgcd  16618  lcmgcdlem  16660  isprm7  16763  4sqlem7  17000  vdwlem1  17037  chnub  18674  met1stc  24643  cfilucfil  24681  nlmvscnlem2  24807  icccmplem2  24946  reconnlem2  24950  xrhmeo  25070  cnheibor  25079  nmoleub2lem3  25239  ipcnlem2  25368  minveclem3b  25552  ivthlem1  25575  ivthlem2  25576  ivth2  25579  ivthle  25580  ivthle2  25581  ovollb2lem  25612  ovolicc2lem4  25644  ovolicc2lem5  25645  ioombl1lem4  25685  uniioombllem4  25710  uniioombllem5  25711  opnmbllem  25725  ismbf3d  25778  mbfi1fseqlem6  25844  itg2gt0  25884  dveflem  26103  dvferm1lem  26108  dvferm2lem  26110  rollelem  26113  rolle  26114  cmvth  26115  mvth  26116  c1liplem1  26120  dvgt0lem1  26126  dvivthlem1  26132  lhop1lem  26137  lhop1  26138  dvcnvrelem1  26141  dvcnvrelem2  26142  dvcvx  26144  dgradd2  26390  aaliou3lem8  26471  aaliou3lem7  26475  ulmdvlem1  26525  itgulm  26533  radcnvlt1  26543  radcnvle  26545  abelthlem7  26563  efcvx  26574  coseq0negpitopi  26630  tangtx  26632  tanabsge  26633  tanord  26665  abslogimle  26700  divlogrlim  26762  logno1  26763  logcnlem3  26771  logcnlem4  26772  logtayl  26787  logccv  26790  cxple  26822  rtprmirr  26887  chordthmlem4  26962  asinsin  27019  atanlogaddlem  27040  atantan  27050  cxp2limlem  27102  logdifbnd  27120  emcllem4  27125  harmonicbnd4  27137  lgamucov  27164  ftalem1  27199  ftalem2  27200  ftalem3  27201  basellem5  27211  basellem8  27214  chpchtsum  27345  bposlem1  27410  lgseisenlem1  27501  lgsquadlem1  27506  lgsquadlem2  27507  lgsquadlem3  27508  2sqreulem1  27572  2sqreunnlem1  27575  chebbnd1lem2  27596  chebbnd1lem3  27597  chtppilimlem1  27599  chto1ub  27602  chpo1ubb  27607  vmadivsumb  27609  dchrisumlem3  27617  mulog2sumlem1  27660  vmalogdivsum2  27664  vmalogdivsum  27665  2vmadivsumlem  27666  selbergb  27675  selberg2b  27678  chpdifbndlem1  27679  selberg3lem2  27684  selberg3  27685  selberg4lem1  27686  selberg4  27687  pntrsumbnd  27692  selberg3r  27695  selberg4r  27696  selberg34r  27697  pntrlog2bndlem1  27703  pntrlog2bndlem2  27704  pntrlog2bndlem3  27705  pntrlog2bndlem4  27706  pntrlog2bndlem5  27707  pntrlog2bndlem6a  27708  pntrlog2bndlem6  27709  pntrlog2bnd  27710  pntpbnd1a  27711  pntpbnd1  27712  pntpbnd2  27713  pntibndlem2  27717  pntlemb  27723  pntlemq  27727  pntlemr  27728  pntlemj  27729  pntlemf  27731  pntlemp  27736  ostth2lem2  27760  axpaschlem  29227  axlowdimlem16  29244  smcnlem  30986  bcm1n  33077  wrdt2ind  33210  cycpmco2lem6  33388  cyc3conja  33414  smatrcl  34127  fiunelros  34505  dya2icoseg  34608  eulerpartlemgc  34693  dstfrvunirn  34806  ballotlemfc0  34824  ballotlemfcc  34825  ballotlemimin  34837  ballotlemsgt1  34842  ballotlemfrcn0  34861  fdvposlt  34927  breprexp  34961  logdivsqrle  34978  hgt750leme  34986  tgoldbachgt  34991  lpadmax  35013  lpadright  35015  subfacval3  35576  erdszelem8  35585  cvmliftlem6  35677  cvmliftlem7  35678  cvmliftlem8  35679  cvmliftlem9  35680  cvmliftlem10  35681  sinccvglem  36059  dnibndlem9  36960  unbdqndv2lem2  36984  knoppndvlem14  36999  knoppndvlem18  37003  knoppndvlem19  37004  poimirlem7  38161  poimirlem15  38169  opnmbllem0  38190  itg2addnclem  38205  itg2addnclem3  38207  itg2addnc  38208  itg2gt0cn  38209  areacirclem1  38242  areacirc  38247  isbnd3  38318  cntotbnd  38330  rrnequiv  38369  lcmineqlem11  42691  lcmineqlem22  42702  3lexlogpow5ineq2  42707  3lexlogpow5ineq5  42712  dvrelogpow2b  42720  aks4d1p1p2  42722  aks4d1p1p4  42723  aks4d1p1p6  42725  aks4d1p1p7  42726  aks4d1p1p5  42727  aks4d1p1  42728  aks4d1p2  42729  aks4d1p3  42730  aks4d1p5  42732  aks4d1p7d1  42734  aks4d1p7  42735  aks4d1p8  42739  hashscontpow1  42773  aks6d1c2lem4  42779  aks6d1c5lem2  42790  sticksstones6  42803  sticksstones12a  42809  sticksstones12  42810  aks6d1c7lem1  42832  unitscyglem2  42848  posqsqznn  42982  redvmptabs  43006  readvrec  43008  fltnltalem  43281  irrapxlem3  43438  pellexlem2  43444  pellfundglb  43499  monotuz  43555  monotoddzzfi  43556  acongrep  43594  cvgdvgrat  44910  hashnzfz2  44918  hashnzfzclim  44919  binomcxplemnotnn0  44953  monoords  45903  xralrple2  45957  reclt0d  45989  reclt0  45993  uzublem  46031  cvgcaule  46092  iooiinicc  46145  iooiinioc  46159  limciccioolb  46224  limcicciooub  46238  lptre2pt  46241  limsupubuzlem  46313  limsup10exlem  46373  icccncfext  46488  cncfiooicclem1  46494  dvdivbd  46524  dvbdfbdioolem1  46529  dvbdfbdioolem2  46530  ioodvbdlimc1lem2  46533  ioodvbdlimc2lem  46535  dvnxpaek  46543  dvnmul  46544  volioc  46573  iblspltprt  46574  itgspltprt  46580  volico  46584  volioore  46591  voliooico  46593  voliccico  46600  stoweidlem1  46602  stoweidlem3  46604  stoweidlem7  46608  stoweidlem24  46625  stoweidlem26  46627  stoweidlem42  46643  wallispilem5  46670  stirlinglem1  46675  stirlinglem6  46680  stirlinglem7  46681  stirlinglem10  46684  stirlinglem12  46686  stirlinglem13  46687  stirlingr  46691  dirkertrigeqlem1  46699  fourierdlem10  46718  fourierdlem11  46719  fourierdlem12  46720  fourierdlem14  46722  fourierdlem15  46723  fourierdlem17  46725  fourierdlem19  46727  fourierdlem30  46738  fourierdlem37  46745  fourierdlem40  46748  fourierdlem41  46749  fourierdlem42  46750  fourierdlem47  46754  fourierdlem48  46755  fourierdlem49  46756  fourierdlem50  46757  fourierdlem51  46758  fourierdlem54  46761  fourierdlem63  46770  fourierdlem64  46771  fourierdlem65  46772  fourierdlem68  46775  fourierdlem73  46780  fourierdlem74  46781  fourierdlem76  46783  fourierdlem77  46784  fourierdlem78  46785  fourierdlem79  46786  fourierdlem81  46788  fourierdlem82  46789  fourierdlem83  46790  fourierdlem92  46799  fourierdlem93  46800  fourierdlem102  46809  fourierdlem103  46810  fourierdlem104  46811  fourierdlem107  46814  fourierdlem111  46818  fourierdlem114  46821  sqwvfoura  46829  sqwvfourb  46830  fouriersw  46832  etransclem19  46854  etransclem23  46858  etransclem35  46870  etransclem41  46876  qndenserrnbllem  46895  iundjiun  47061  carageniuncllem2  47123  caratheodorylem1  47127  hoicvr  47149  ovnsubaddlem1  47171  hsphoidmvle2  47186  hoidmv1lelem1  47192  hoidmv1lelem2  47193  hoidmvlelem1  47196  hoidmvlelem2  47197  hoidmvlelem3  47198  hoiqssbllem1  47223  hoiqssbllem2  47224  volico2  47242  iinhoiicclem  47274  iunhoiioolem  47276  vonioolem2  47282  vonicclem2  47285  pimdecfgtioo  47318  pimincfltioo  47319  smflimlem4  47375  smfmullem1  47392  smflimsuplem4  47424  gpg3kgrtriexlem4  48735  gpg3kgrtriexlem6  48737  expnegico01  49178  eenglngeehlnmlem2  49398  inlinecirc02plem  49446