Theorem ltled 11169

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

Syntax hints:   → wi 4   ∈ wcel 2104   class class class wbr 5081  ℝcr 10916   < clt 11055   ≤ cle 11056

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2707  ax-sep 5232  ax-nul 5239  ax-pow 5297  ax-pr 5361  ax-un 7620  ax-resscn 10974  ax-pre-lttri 10991

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rab 3287  df-v 3439  df-sbc 3722  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4566  df-pr 4568  df-op 4572  df-uni 4845  df-br 5082  df-opab 5144  df-mpt 5165  df-id 5500  df-xp 5606  df-rel 5607  df-cnv 5608  df-co 5609  df-dm 5610  df-rn 5611  df-res 5612  df-ima 5613  df-iota 6410  df-fun 6460  df-fn 6461  df-f 6462  df-f1 6463  df-fo 6464  df-f1o 6465  df-fv 6466  df-er 8529  df-en 8765  df-dom 8766  df-sdom 8767  df-pnf 11057  df-mnf 11058  df-xr 11059  df-ltxr 11060  df-le 11061

This theorem is referenced by:  ltnsymd  11170  mulge0  11539  msqge0  11542  addgt0d  11596  lt2addd  11644  lt2msq1  11905  uzwo3  12729  fznatpl1  13356  flflp1  13573  modaddmodup  13700  expmulnbnd  13996  fzsdom2  14188  repswcshw  14570  isercolllem1  15421  caucvgrlem  15429  climcnds  15608  geomulcvg  15633  mertenslem1  15641  ruclem2  15986  ruclem12  15995  bitsfzo  16187  bitsmod  16188  lcmgcdlem  16356  isprm7  16458  4sqlem7  16690  vdwlem1  16727  met1stc  23722  cfilucfil  23760  nlmvscnlem2  23894  icccmplem2  24031  reconnlem2  24035  xrhmeo  24154  cnheibor  24163  nmoleub2lem3  24323  ipcnlem2  24453  minveclem3b  24637  ivthlem1  24660  ivthlem2  24661  ivth2  24664  ivthle  24665  ivthle2  24666  ovollb2lem  24697  ovolicc2lem4  24729  ovolicc2lem5  24730  ioombl1lem4  24770  uniioombllem4  24795  uniioombllem5  24796  opnmbllem  24810  ismbf3d  24863  mbfi1fseqlem6  24930  itg2gt0  24970  dveflem  25188  dvferm1lem  25193  dvferm2lem  25195  rollelem  25198  rolle  25199  cmvth  25200  mvth  25201  c1liplem1  25205  dvgt0lem1  25211  dvivthlem1  25217  lhop1lem  25222  lhop1  25223  dvcnvrelem1  25226  dvcnvrelem2  25227  dvcvx  25229  dgradd2  25474  aaliou3lem8  25550  aaliou3lem7  25554  ulmdvlem1  25604  itgulm  25612  radcnvlt1  25622  radcnvle  25624  abelthlem7  25642  efcvx  25653  coseq0negpitopi  25705  tangtx  25707  tanabsge  25708  tanord  25739  abslogimle  25774  divlogrlim  25835  logno1  25836  logcnlem3  25844  logcnlem4  25845  logtayl  25860  logccv  25863  cxple  25895  chordthmlem4  26030  asinsin  26087  atanlogaddlem  26108  atantan  26118  cxp2limlem  26170  logdifbnd  26188  emcllem4  26193  harmonicbnd4  26205  lgamucov  26232  ftalem1  26267  ftalem2  26268  ftalem3  26269  basellem5  26279  basellem8  26282  chpchtsum  26412  bposlem1  26477  lgseisenlem1  26568  lgsquadlem1  26573  lgsquadlem2  26574  lgsquadlem3  26575  2sqreulem1  26639  2sqreunnlem1  26642  chebbnd1lem2  26663  chebbnd1lem3  26664  chtppilimlem1  26666  chto1ub  26669  chpo1ubb  26674  vmadivsumb  26676  dchrisumlem3  26684  mulog2sumlem1  26727  vmalogdivsum2  26731  vmalogdivsum  26732  2vmadivsumlem  26733  selbergb  26742  selberg2b  26745  chpdifbndlem1  26746  selberg3lem2  26751  selberg3  26752  selberg4lem1  26753  selberg4  26754  pntrsumbnd  26759  selberg3r  26762  selberg4r  26763  selberg34r  26764  pntrlog2bndlem1  26770  pntrlog2bndlem2  26771  pntrlog2bndlem3  26772  pntrlog2bndlem4  26773  pntrlog2bndlem5  26774  pntrlog2bndlem6a  26775  pntrlog2bndlem6  26776  pntrlog2bnd  26777  pntpbnd1a  26778  pntpbnd1  26779  pntpbnd2  26780  pntibndlem2  26784  pntlemb  26790  pntlemq  26794  pntlemr  26795  pntlemj  26796  pntlemf  26798  pntlemp  26803  ostth2lem2  26827  axpaschlem  27353  axlowdimlem16  27370  smcnlem  29104  bcm1n  31161  wrdt2ind  31270  cycpmco2lem6  31443  cyc3conja  31469  smatrcl  31791  fiunelros  32187  dya2icoseg  32289  eulerpartlemgc  32374  dstfrvunirn  32486  ballotlemfc0  32504  ballotlemfcc  32505  ballotlemimin  32517  ballotlemsgt1  32522  ballotlemfrcn0  32541  sgnmul  32554  fdvposlt  32624  breprexp  32658  logdivsqrle  32675  hgt750leme  32683  tgoldbachgt  32688  lpadmax  32707  lpadright  32709  subfacval3  33196  erdszelem8  33205  cvmliftlem6  33297  cvmliftlem7  33298  cvmliftlem8  33299  cvmliftlem9  33300  cvmliftlem10  33301  sinccvglem  33675  dnibndlem9  34711  unbdqndv2lem2  34735  knoppndvlem14  34750  knoppndvlem18  34754  knoppndvlem19  34755  poimirlem7  35828  poimirlem15  35836  opnmbllem0  35857  itg2addnclem  35872  itg2addnclem3  35874  itg2addnc  35875  itg2gt0cn  35876  areacirclem1  35909  areacirc  35914  isbnd3  35986  cntotbnd  35998  rrnequiv  36037  lcmineqlem11  40089  lcmineqlem22  40100  3lexlogpow5ineq2  40105  3lexlogpow5ineq5  40110  dvrelogpow2b  40118  aks4d1p1p2  40120  aks4d1p1p4  40121  aks4d1p1p6  40123  aks4d1p1p7  40124  aks4d1p1p5  40125  aks4d1p1  40126  aks4d1p2  40127  aks4d1p3  40128  aks4d1p5  40130  aks4d1p7d1  40132  aks4d1p7  40133  aks4d1p8  40137  sticksstones6  40149  sticksstones12a  40155  sticksstones12  40156  metakunt7  40173  metakunt29  40195  metakunt30  40196  nn0rppwr  40370  nn0expgcd  40372  posqsqznn  40380  rtprmirr  40384  fltnltalem  40536  irrapxlem3  40683  pellexlem2  40689  pellfundglb  40744  monotuz  40801  monotoddzzfi  40802  acongrep  40840  cvgdvgrat  41969  hashnzfz2  41977  hashnzfzclim  41978  binomcxplemnotnn0  42012  monoords  42884  xralrple2  42941  reclt0d  42974  reclt0  42979  uzublem  43018  iooiinicc  43129  iooiinioc  43143  limciccioolb  43211  limcicciooub  43227  lptre2pt  43230  limsupubuzlem  43302  limsup10exlem  43362  icccncfext  43477  cncfiooicclem1  43483  dvdivbd  43513  dvbdfbdioolem1  43518  dvbdfbdioolem2  43519  ioodvbdlimc1lem2  43522  ioodvbdlimc2lem  43524  dvnxpaek  43532  dvnmul  43533  volioc  43562  iblspltprt  43563  itgspltprt  43569  volico  43573  volioore  43580  voliooico  43582  voliccico  43589  stoweidlem1  43591  stoweidlem3  43593  stoweidlem7  43597  stoweidlem24  43614  stoweidlem26  43616  stoweidlem42  43632  wallispilem5  43659  stirlinglem1  43664  stirlinglem6  43669  stirlinglem7  43670  stirlinglem10  43673  stirlinglem12  43675  stirlinglem13  43676  stirlingr  43680  dirkertrigeqlem1  43688  fourierdlem10  43707  fourierdlem11  43708  fourierdlem12  43709  fourierdlem14  43711  fourierdlem15  43712  fourierdlem17  43714  fourierdlem19  43716  fourierdlem30  43727  fourierdlem37  43734  fourierdlem40  43737  fourierdlem41  43738  fourierdlem42  43739  fourierdlem47  43743  fourierdlem48  43744  fourierdlem49  43745  fourierdlem50  43746  fourierdlem51  43747  fourierdlem54  43750  fourierdlem63  43759  fourierdlem64  43760  fourierdlem65  43761  fourierdlem68  43764  fourierdlem73  43769  fourierdlem74  43770  fourierdlem76  43772  fourierdlem77  43773  fourierdlem78  43774  fourierdlem79  43775  fourierdlem81  43777  fourierdlem82  43778  fourierdlem83  43779  fourierdlem92  43788  fourierdlem93  43789  fourierdlem102  43798  fourierdlem103  43799  fourierdlem104  43800  fourierdlem107  43803  fourierdlem111  43807  fourierdlem114  43810  sqwvfoura  43818  sqwvfourb  43819  fouriersw  43821  etransclem19  43843  etransclem23  43847  etransclem35  43859  etransclem41  43865  qndenserrnbllem  43884  iundjiun  44048  carageniuncllem2  44110  caratheodorylem1  44114  hoicvr  44136  ovnsubaddlem1  44158  hsphoidmvle2  44173  hoidmv1lelem1  44179  hoidmv1lelem2  44180  hoidmvlelem1  44183  hoidmvlelem2  44184  hoidmvlelem3  44185  hoiqssbllem1  44210  hoiqssbllem2  44211  volico2  44229  iinhoiicclem  44261  iunhoiioolem  44263  vonioolem2  44269  vonicclem2  44272  pimdecfgtioo  44305  pimincfltioo  44306  smflimlem4  44362  smfmullem1  44379  smflimsuplem4  44410  expnegico01  45917  eenglngeehlnmlem2  46142  inlinecirc02plem  46190