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 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  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  42980  redvmptabs  43004  readvrec  43006  fltnltalem  43279  irrapxlem3  43436  pellexlem2  43442  pellfundglb  43497  monotuz  43553  monotoddzzfi  43554  acongrep  43592  cvgdvgrat  44908  hashnzfz2  44916  hashnzfzclim  44917  binomcxplemnotnn0  44951  monoords  45901  xralrple2  45955  reclt0d  45987  reclt0  45991  uzublem  46029  cvgcaule  46090  iooiinicc  46143  iooiinioc  46157  limciccioolb  46222  limcicciooub  46236  lptre2pt  46239  limsupubuzlem  46311  limsup10exlem  46371  icccncfext  46486  cncfiooicclem1  46492  dvdivbd  46522  dvbdfbdioolem1  46527  dvbdfbdioolem2  46528  ioodvbdlimc1lem2  46531  ioodvbdlimc2lem  46533  dvnxpaek  46541  dvnmul  46542  volioc  46571  iblspltprt  46572  itgspltprt  46578  volico  46582  volioore  46589  voliooico  46591  voliccico  46598  stoweidlem1  46600  stoweidlem3  46602  stoweidlem7  46606  stoweidlem24  46623  stoweidlem26  46625  stoweidlem42  46641  wallispilem5  46668  stirlinglem1  46673  stirlinglem6  46678  stirlinglem7  46679  stirlinglem10  46682  stirlinglem12  46684  stirlinglem13  46685  stirlingr  46689  dirkertrigeqlem1  46697  fourierdlem10  46716  fourierdlem11  46717  fourierdlem12  46718  fourierdlem14  46720  fourierdlem15  46721  fourierdlem17  46723  fourierdlem19  46725  fourierdlem30  46736  fourierdlem37  46743  fourierdlem40  46746  fourierdlem41  46747  fourierdlem42  46748  fourierdlem47  46752  fourierdlem48  46753  fourierdlem49  46754  fourierdlem50  46755  fourierdlem51  46756  fourierdlem54  46759  fourierdlem63  46768  fourierdlem64  46769  fourierdlem65  46770  fourierdlem68  46773  fourierdlem73  46778  fourierdlem74  46779  fourierdlem76  46781  fourierdlem77  46782  fourierdlem78  46783  fourierdlem79  46784  fourierdlem81  46786  fourierdlem82  46787  fourierdlem83  46788  fourierdlem92  46797  fourierdlem93  46798  fourierdlem102  46807  fourierdlem103  46808  fourierdlem104  46809  fourierdlem107  46812  fourierdlem111  46816  fourierdlem114  46819  sqwvfoura  46827  sqwvfourb  46828  fouriersw  46830  etransclem19  46852  etransclem23  46856  etransclem35  46868  etransclem41  46874  qndenserrnbllem  46893  iundjiun  47059  carageniuncllem2  47121  caratheodorylem1  47125  hoicvr  47147  ovnsubaddlem1  47169  hsphoidmvle2  47184  hoidmv1lelem1  47190  hoidmv1lelem2  47191  hoidmvlelem1  47194  hoidmvlelem2  47195  hoidmvlelem3  47196  hoiqssbllem1  47221  hoiqssbllem2  47222  volico2  47240  iinhoiicclem  47272  iunhoiioolem  47274  vonioolem2  47280  vonicclem2  47283  pimdecfgtioo  47316  pimincfltioo  47317  smflimlem4  47373  smfmullem1  47390  smflimsuplem4  47422  gpg3kgrtriexlem4  48733  gpg3kgrtriexlem6  48735  expnegico01  49176  eenglngeehlnmlem2  49396  inlinecirc02plem  49444