Theorem ltled 11272

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

Syntax hints:   → wi 4   ∈ wcel 2113   class class class wbr 5095  ℝcr 11016   < clt 11157   ≤ cle 11158

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7677  ax-resscn 11074  ax-pre-lttri 11091

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-nel 3034  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5516  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496  df-fv 6497  df-er 8631  df-en 8880  df-dom 8881  df-sdom 8882  df-pnf 11159  df-mnf 11160  df-xr 11161  df-ltxr 11162  df-le 11163

This theorem is referenced by:  ltnsymd  11273  mulge0  11646  msqge0  11649  addgt0d  11703  lt2addd  11751  lt2msq1  12017  uzwo3  12847  fznatpl1  13485  flflp1  13718  modaddmodup  13848  expmulnbnd  14149  fzsdom2  14342  repswcshw  14726  isercolllem1  15579  caucvgrlem  15587  climcnds  15765  geomulcvg  15790  mertenslem1  15798  ruclem2  16148  ruclem12  16157  bitsfzo  16353  bitsmod  16354  nn0rppwr  16479  nn0expgcd  16482  lcmgcdlem  16524  isprm7  16626  4sqlem7  16863  vdwlem1  16900  chnub  18536  met1stc  24456  cfilucfil  24494  nlmvscnlem2  24620  icccmplem2  24759  reconnlem2  24763  xrhmeo  24891  cnheibor  24901  nmoleub2lem3  25062  ipcnlem2  25191  minveclem3b  25375  ivthlem1  25399  ivthlem2  25400  ivth2  25403  ivthle  25404  ivthle2  25405  ovollb2lem  25436  ovolicc2lem4  25468  ovolicc2lem5  25469  ioombl1lem4  25509  uniioombllem4  25534  uniioombllem5  25535  opnmbllem  25549  ismbf3d  25602  mbfi1fseqlem6  25668  itg2gt0  25708  dveflem  25930  dvferm1lem  25935  dvferm2lem  25937  rollelem  25940  rolle  25941  cmvth  25942  cmvthOLD  25943  mvth  25944  c1liplem1  25948  dvgt0lem1  25954  dvivthlem1  25960  lhop1lem  25965  lhop1  25966  dvcnvrelem1  25969  dvcnvrelem2  25970  dvcvx  25972  dgradd2  26221  aaliou3lem8  26300  aaliou3lem7  26304  ulmdvlem1  26356  itgulm  26364  radcnvlt1  26374  radcnvle  26376  abelthlem7  26395  efcvx  26406  coseq0negpitopi  26459  tangtx  26461  tanabsge  26462  tanord  26494  abslogimle  26529  divlogrlim  26591  logno1  26592  logcnlem3  26600  logcnlem4  26601  logtayl  26616  logccv  26619  cxple  26651  rtprmirr  26717  chordthmlem4  26792  asinsin  26849  atanlogaddlem  26870  atantan  26880  cxp2limlem  26933  logdifbnd  26951  emcllem4  26956  harmonicbnd4  26968  lgamucov  26995  ftalem1  27030  ftalem2  27031  ftalem3  27032  basellem5  27042  basellem8  27045  chpchtsum  27177  bposlem1  27242  lgseisenlem1  27333  lgsquadlem1  27338  lgsquadlem2  27339  lgsquadlem3  27340  2sqreulem1  27404  2sqreunnlem1  27407  chebbnd1lem2  27428  chebbnd1lem3  27429  chtppilimlem1  27431  chto1ub  27434  chpo1ubb  27439  vmadivsumb  27441  dchrisumlem3  27449  mulog2sumlem1  27492  vmalogdivsum2  27496  vmalogdivsum  27497  2vmadivsumlem  27498  selbergb  27507  selberg2b  27510  chpdifbndlem1  27511  selberg3lem2  27516  selberg3  27517  selberg4lem1  27518  selberg4  27519  pntrsumbnd  27524  selberg3r  27527  selberg4r  27528  selberg34r  27529  pntrlog2bndlem1  27535  pntrlog2bndlem2  27536  pntrlog2bndlem3  27537  pntrlog2bndlem4  27538  pntrlog2bndlem5  27539  pntrlog2bndlem6a  27540  pntrlog2bndlem6  27541  pntrlog2bnd  27542  pntpbnd1a  27543  pntpbnd1  27544  pntpbnd2  27545  pntibndlem2  27549  pntlemb  27555  pntlemq  27559  pntlemr  27560  pntlemj  27561  pntlemf  27563  pntlemp  27568  ostth2lem2  27592  axpaschlem  28939  axlowdimlem16  28956  smcnlem  30698  bcm1n  32803  sgnmul  32844  wrdt2ind  32963  cycpmco2lem6  33141  cyc3conja  33167  smatrcl  33881  fiunelros  34259  dya2icoseg  34362  eulerpartlemgc  34447  dstfrvunirn  34560  ballotlemfc0  34578  ballotlemfcc  34579  ballotlemimin  34591  ballotlemsgt1  34596  ballotlemfrcn0  34615  fdvposlt  34684  breprexp  34718  logdivsqrle  34735  hgt750leme  34743  tgoldbachgt  34748  lpadmax  34767  lpadright  34769  subfacval3  35305  erdszelem8  35314  cvmliftlem6  35406  cvmliftlem7  35407  cvmliftlem8  35408  cvmliftlem9  35409  cvmliftlem10  35410  sinccvglem  35788  dnibndlem9  36602  unbdqndv2lem2  36626  knoppndvlem14  36641  knoppndvlem18  36645  knoppndvlem19  36646  poimirlem7  37740  poimirlem15  37748  opnmbllem0  37769  itg2addnclem  37784  itg2addnclem3  37786  itg2addnc  37787  itg2gt0cn  37788  areacirclem1  37821  areacirc  37826  isbnd3  37897  cntotbnd  37909  rrnequiv  37948  lcmineqlem11  42205  lcmineqlem22  42216  3lexlogpow5ineq2  42221  3lexlogpow5ineq5  42226  dvrelogpow2b  42234  aks4d1p1p2  42236  aks4d1p1p4  42237  aks4d1p1p6  42239  aks4d1p1p7  42240  aks4d1p1p5  42241  aks4d1p1  42242  aks4d1p2  42243  aks4d1p3  42244  aks4d1p5  42246  aks4d1p7d1  42248  aks4d1p7  42249  aks4d1p8  42253  hashscontpow1  42287  aks6d1c2lem4  42293  aks6d1c5lem2  42304  sticksstones6  42317  sticksstones12a  42323  sticksstones12  42324  aks6d1c7lem1  42346  unitscyglem2  42362  posqsqznn  42506  redvmptabs  42530  readvrec  42532  fltnltalem  42820  irrapxlem3  42981  pellexlem2  42987  pellfundglb  43042  monotuz  43098  monotoddzzfi  43099  acongrep  43137  cvgdvgrat  44470  hashnzfz2  44478  hashnzfzclim  44479  binomcxplemnotnn0  44513  monoords  45461  xralrple2  45515  reclt0d  45547  reclt0  45551  uzublem  45590  cvgcaule  45651  iooiinicc  45704  iooiinioc  45718  limciccioolb  45783  limcicciooub  45797  lptre2pt  45800  limsupubuzlem  45872  limsup10exlem  45932  icccncfext  46047  cncfiooicclem1  46053  dvdivbd  46083  dvbdfbdioolem1  46088  dvbdfbdioolem2  46089  ioodvbdlimc1lem2  46092  ioodvbdlimc2lem  46094  dvnxpaek  46102  dvnmul  46103  volioc  46132  iblspltprt  46133  itgspltprt  46139  volico  46143  volioore  46150  voliooico  46152  voliccico  46159  stoweidlem1  46161  stoweidlem3  46163  stoweidlem7  46167  stoweidlem24  46184  stoweidlem26  46186  stoweidlem42  46202  wallispilem5  46229  stirlinglem1  46234  stirlinglem6  46239  stirlinglem7  46240  stirlinglem10  46243  stirlinglem12  46245  stirlinglem13  46246  stirlingr  46250  dirkertrigeqlem1  46258  fourierdlem10  46277  fourierdlem11  46278  fourierdlem12  46279  fourierdlem14  46281  fourierdlem15  46282  fourierdlem17  46284  fourierdlem19  46286  fourierdlem30  46297  fourierdlem37  46304  fourierdlem40  46307  fourierdlem41  46308  fourierdlem42  46309  fourierdlem47  46313  fourierdlem48  46314  fourierdlem49  46315  fourierdlem50  46316  fourierdlem51  46317  fourierdlem54  46320  fourierdlem63  46329  fourierdlem64  46330  fourierdlem65  46331  fourierdlem68  46334  fourierdlem73  46339  fourierdlem74  46340  fourierdlem76  46342  fourierdlem77  46343  fourierdlem78  46344  fourierdlem79  46345  fourierdlem81  46347  fourierdlem82  46348  fourierdlem83  46349  fourierdlem92  46358  fourierdlem93  46359  fourierdlem102  46368  fourierdlem103  46369  fourierdlem104  46370  fourierdlem107  46373  fourierdlem111  46377  fourierdlem114  46380  sqwvfoura  46388  sqwvfourb  46389  fouriersw  46391  etransclem19  46413  etransclem23  46417  etransclem35  46429  etransclem41  46435  qndenserrnbllem  46454  iundjiun  46620  carageniuncllem2  46682  caratheodorylem1  46686  hoicvr  46708  ovnsubaddlem1  46730  hsphoidmvle2  46745  hoidmv1lelem1  46751  hoidmv1lelem2  46752  hoidmvlelem1  46755  hoidmvlelem2  46756  hoidmvlelem3  46757  hoiqssbllem1  46782  hoiqssbllem2  46783  volico2  46801  iinhoiicclem  46833  iunhoiioolem  46835  vonioolem2  46841  vonicclem2  46844  pimdecfgtioo  46877  pimincfltioo  46878  smflimlem4  46934  smfmullem1  46951  smflimsuplem4  46983  gpg3kgrtriexlem4  48248  gpg3kgrtriexlem6  48250  expnegico01  48680  eenglngeehlnmlem2  48900  inlinecirc02plem  48948