Theorem ltled 11285

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

Syntax hints:   → wi 4   ∈ wcel 2114   class class class wbr 5086  ℝcr 11028   < clt 11170   ≤ cle 11171

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pow 5302  ax-pr 5370  ax-un 7682  ax-resscn 11086  ax-pre-lttri 11103

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-er 8636  df-en 8887  df-dom 8888  df-sdom 8889  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176

This theorem is referenced by:  ltnsymd  11286  mulge0  11659  msqge0  11662  addgt0d  11716  lt2addd  11764  lt2msq1  12031  uzwo3  12884  fznatpl1  13523  flflp1  13757  modaddmodup  13887  expmulnbnd  14188  fzsdom2  14381  repswcshw  14765  isercolllem1  15618  caucvgrlem  15626  climcnds  15807  geomulcvg  15832  mertenslem1  15840  ruclem2  16190  ruclem12  16199  bitsfzo  16395  bitsmod  16396  nn0rppwr  16521  nn0expgcd  16524  lcmgcdlem  16566  isprm7  16669  4sqlem7  16906  vdwlem1  16943  chnub  18579  met1stc  24496  cfilucfil  24534  nlmvscnlem2  24660  icccmplem2  24799  reconnlem2  24803  xrhmeo  24923  cnheibor  24932  nmoleub2lem3  25092  ipcnlem2  25221  minveclem3b  25405  ivthlem1  25428  ivthlem2  25429  ivth2  25432  ivthle  25433  ivthle2  25434  ovollb2lem  25465  ovolicc2lem4  25497  ovolicc2lem5  25498  ioombl1lem4  25538  uniioombllem4  25563  uniioombllem5  25564  opnmbllem  25578  ismbf3d  25631  mbfi1fseqlem6  25697  itg2gt0  25737  dveflem  25956  dvferm1lem  25961  dvferm2lem  25963  rollelem  25966  rolle  25967  cmvth  25968  mvth  25969  c1liplem1  25973  dvgt0lem1  25979  dvivthlem1  25985  lhop1lem  25990  lhop1  25991  dvcnvrelem1  25994  dvcnvrelem2  25995  dvcvx  25997  dgradd2  26243  aaliou3lem8  26322  aaliou3lem7  26326  ulmdvlem1  26378  itgulm  26386  radcnvlt1  26396  radcnvle  26398  abelthlem7  26416  efcvx  26427  coseq0negpitopi  26480  tangtx  26482  tanabsge  26483  tanord  26515  abslogimle  26550  divlogrlim  26612  logno1  26613  logcnlem3  26621  logcnlem4  26622  logtayl  26637  logccv  26640  cxple  26672  rtprmirr  26737  chordthmlem4  26812  asinsin  26869  atanlogaddlem  26890  atantan  26900  cxp2limlem  26953  logdifbnd  26971  emcllem4  26976  harmonicbnd4  26988  lgamucov  27015  ftalem1  27050  ftalem2  27051  ftalem3  27052  basellem5  27062  basellem8  27065  chpchtsum  27196  bposlem1  27261  lgseisenlem1  27352  lgsquadlem1  27357  lgsquadlem2  27358  lgsquadlem3  27359  2sqreulem1  27423  2sqreunnlem1  27426  chebbnd1lem2  27447  chebbnd1lem3  27448  chtppilimlem1  27450  chto1ub  27453  chpo1ubb  27458  vmadivsumb  27460  dchrisumlem3  27468  mulog2sumlem1  27511  vmalogdivsum2  27515  vmalogdivsum  27516  2vmadivsumlem  27517  selbergb  27526  selberg2b  27529  chpdifbndlem1  27530  selberg3lem2  27535  selberg3  27536  selberg4lem1  27537  selberg4  27538  pntrsumbnd  27543  selberg3r  27546  selberg4r  27547  selberg34r  27548  pntrlog2bndlem1  27554  pntrlog2bndlem2  27555  pntrlog2bndlem3  27556  pntrlog2bndlem4  27557  pntrlog2bndlem5  27558  pntrlog2bndlem6a  27559  pntrlog2bndlem6  27560  pntrlog2bnd  27561  pntpbnd1a  27562  pntpbnd1  27563  pntpbnd2  27564  pntibndlem2  27568  pntlemb  27574  pntlemq  27578  pntlemr  27579  pntlemj  27580  pntlemf  27582  pntlemp  27587  ostth2lem2  27611  axpaschlem  29023  axlowdimlem16  29040  smcnlem  30783  bcm1n  32883  sgnmul  32923  wrdt2ind  33028  cycpmco2lem6  33207  cyc3conja  33233  smatrcl  33956  fiunelros  34334  dya2icoseg  34437  eulerpartlemgc  34522  dstfrvunirn  34635  ballotlemfc0  34653  ballotlemfcc  34654  ballotlemimin  34666  ballotlemsgt1  34671  ballotlemfrcn0  34690  fdvposlt  34759  breprexp  34793  logdivsqrle  34810  hgt750leme  34818  tgoldbachgt  34823  lpadmax  34842  lpadright  34844  subfacval3  35387  erdszelem8  35396  cvmliftlem6  35488  cvmliftlem7  35489  cvmliftlem8  35490  cvmliftlem9  35491  cvmliftlem10  35492  sinccvglem  35870  dnibndlem9  36762  unbdqndv2lem2  36786  knoppndvlem14  36801  knoppndvlem18  36805  knoppndvlem19  36806  poimirlem7  37962  poimirlem15  37970  opnmbllem0  37991  itg2addnclem  38006  itg2addnclem3  38008  itg2addnc  38009  itg2gt0cn  38010  areacirclem1  38043  areacirc  38048  isbnd3  38119  cntotbnd  38131  rrnequiv  38170  lcmineqlem11  42492  lcmineqlem22  42503  3lexlogpow5ineq2  42508  3lexlogpow5ineq5  42513  dvrelogpow2b  42521  aks4d1p1p2  42523  aks4d1p1p4  42524  aks4d1p1p6  42526  aks4d1p1p7  42527  aks4d1p1p5  42528  aks4d1p1  42529  aks4d1p2  42530  aks4d1p3  42531  aks4d1p5  42533  aks4d1p7d1  42535  aks4d1p7  42536  aks4d1p8  42540  hashscontpow1  42574  aks6d1c2lem4  42580  aks6d1c5lem2  42591  sticksstones6  42604  sticksstones12a  42610  sticksstones12  42611  aks6d1c7lem1  42633  unitscyglem2  42649  posqsqznn  42782  redvmptabs  42806  readvrec  42808  fltnltalem  43109  irrapxlem3  43270  pellexlem2  43276  pellfundglb  43331  monotuz  43387  monotoddzzfi  43388  acongrep  43426  cvgdvgrat  44758  hashnzfz2  44766  hashnzfzclim  44767  binomcxplemnotnn0  44801  monoords  45748  xralrple2  45802  reclt0d  45834  reclt0  45838  uzublem  45876  cvgcaule  45937  iooiinicc  45990  iooiinioc  46004  limciccioolb  46069  limcicciooub  46083  lptre2pt  46086  limsupubuzlem  46158  limsup10exlem  46218  icccncfext  46333  cncfiooicclem1  46339  dvdivbd  46369  dvbdfbdioolem1  46374  dvbdfbdioolem2  46375  ioodvbdlimc1lem2  46378  ioodvbdlimc2lem  46380  dvnxpaek  46388  dvnmul  46389  volioc  46418  iblspltprt  46419  itgspltprt  46425  volico  46429  volioore  46436  voliooico  46438  voliccico  46445  stoweidlem1  46447  stoweidlem3  46449  stoweidlem7  46453  stoweidlem24  46470  stoweidlem26  46472  stoweidlem42  46488  wallispilem5  46515  stirlinglem1  46520  stirlinglem6  46525  stirlinglem7  46526  stirlinglem10  46529  stirlinglem12  46531  stirlinglem13  46532  stirlingr  46536  dirkertrigeqlem1  46544  fourierdlem10  46563  fourierdlem11  46564  fourierdlem12  46565  fourierdlem14  46567  fourierdlem15  46568  fourierdlem17  46570  fourierdlem19  46572  fourierdlem30  46583  fourierdlem37  46590  fourierdlem40  46593  fourierdlem41  46594  fourierdlem42  46595  fourierdlem47  46599  fourierdlem48  46600  fourierdlem49  46601  fourierdlem50  46602  fourierdlem51  46603  fourierdlem54  46606  fourierdlem63  46615  fourierdlem64  46616  fourierdlem65  46617  fourierdlem68  46620  fourierdlem73  46625  fourierdlem74  46626  fourierdlem76  46628  fourierdlem77  46629  fourierdlem78  46630  fourierdlem79  46631  fourierdlem81  46633  fourierdlem82  46634  fourierdlem83  46635  fourierdlem92  46644  fourierdlem93  46645  fourierdlem102  46654  fourierdlem103  46655  fourierdlem104  46656  fourierdlem107  46659  fourierdlem111  46663  fourierdlem114  46666  sqwvfoura  46674  sqwvfourb  46675  fouriersw  46677  etransclem19  46699  etransclem23  46703  etransclem35  46715  etransclem41  46721  qndenserrnbllem  46740  iundjiun  46906  carageniuncllem2  46968  caratheodorylem1  46972  hoicvr  46994  ovnsubaddlem1  47016  hsphoidmvle2  47031  hoidmv1lelem1  47037  hoidmv1lelem2  47038  hoidmvlelem1  47041  hoidmvlelem2  47042  hoidmvlelem3  47043  hoiqssbllem1  47068  hoiqssbllem2  47069  volico2  47087  iinhoiicclem  47119  iunhoiioolem  47121  vonioolem2  47127  vonicclem2  47130  pimdecfgtioo  47163  pimincfltioo  47164  smflimlem4  47220  smfmullem1  47237  smflimsuplem4  47269  gpg3kgrtriexlem4  48574  gpg3kgrtriexlem6  48576  expnegico01  49006  eenglngeehlnmlem2  49226  inlinecirc02plem  49274