Theorem ltled 11281

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

Syntax hints:   → wi 4   ∈ wcel 2113   class class class wbr 5098  ℝcr 11025   < clt 11166   ≤ cle 11167

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 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680  ax-resscn 11083  ax-pre-lttri 11100

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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-mpt 5180  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 8635  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11168  df-mnf 11169  df-xr 11170  df-ltxr 11171  df-le 11172

This theorem is referenced by:  ltnsymd  11282  mulge0  11655  msqge0  11658  addgt0d  11712  lt2addd  11760  lt2msq1  12026  uzwo3  12856  fznatpl1  13494  flflp1  13727  modaddmodup  13857  expmulnbnd  14158  fzsdom2  14351  repswcshw  14735  isercolllem1  15588  caucvgrlem  15596  climcnds  15774  geomulcvg  15799  mertenslem1  15807  ruclem2  16157  ruclem12  16166  bitsfzo  16362  bitsmod  16363  nn0rppwr  16488  nn0expgcd  16491  lcmgcdlem  16533  isprm7  16635  4sqlem7  16872  vdwlem1  16909  chnub  18545  met1stc  24465  cfilucfil  24503  nlmvscnlem2  24629  icccmplem2  24768  reconnlem2  24772  xrhmeo  24900  cnheibor  24910  nmoleub2lem3  25071  ipcnlem2  25200  minveclem3b  25384  ivthlem1  25408  ivthlem2  25409  ivth2  25412  ivthle  25413  ivthle2  25414  ovollb2lem  25445  ovolicc2lem4  25477  ovolicc2lem5  25478  ioombl1lem4  25518  uniioombllem4  25543  uniioombllem5  25544  opnmbllem  25558  ismbf3d  25611  mbfi1fseqlem6  25677  itg2gt0  25717  dveflem  25939  dvferm1lem  25944  dvferm2lem  25946  rollelem  25949  rolle  25950  cmvth  25951  cmvthOLD  25952  mvth  25953  c1liplem1  25957  dvgt0lem1  25963  dvivthlem1  25969  lhop1lem  25974  lhop1  25975  dvcnvrelem1  25978  dvcnvrelem2  25979  dvcvx  25981  dgradd2  26230  aaliou3lem8  26309  aaliou3lem7  26313  ulmdvlem1  26365  itgulm  26373  radcnvlt1  26383  radcnvle  26385  abelthlem7  26404  efcvx  26415  coseq0negpitopi  26468  tangtx  26470  tanabsge  26471  tanord  26503  abslogimle  26538  divlogrlim  26600  logno1  26601  logcnlem3  26609  logcnlem4  26610  logtayl  26625  logccv  26628  cxple  26660  rtprmirr  26726  chordthmlem4  26801  asinsin  26858  atanlogaddlem  26879  atantan  26889  cxp2limlem  26942  logdifbnd  26960  emcllem4  26965  harmonicbnd4  26977  lgamucov  27004  ftalem1  27039  ftalem2  27040  ftalem3  27041  basellem5  27051  basellem8  27054  chpchtsum  27186  bposlem1  27251  lgseisenlem1  27342  lgsquadlem1  27347  lgsquadlem2  27348  lgsquadlem3  27349  2sqreulem1  27413  2sqreunnlem1  27416  chebbnd1lem2  27437  chebbnd1lem3  27438  chtppilimlem1  27440  chto1ub  27443  chpo1ubb  27448  vmadivsumb  27450  dchrisumlem3  27458  mulog2sumlem1  27501  vmalogdivsum2  27505  vmalogdivsum  27506  2vmadivsumlem  27507  selbergb  27516  selberg2b  27519  chpdifbndlem1  27520  selberg3lem2  27525  selberg3  27526  selberg4lem1  27527  selberg4  27528  pntrsumbnd  27533  selberg3r  27536  selberg4r  27537  selberg34r  27538  pntrlog2bndlem1  27544  pntrlog2bndlem2  27545  pntrlog2bndlem3  27546  pntrlog2bndlem4  27547  pntrlog2bndlem5  27548  pntrlog2bndlem6a  27549  pntrlog2bndlem6  27550  pntrlog2bnd  27551  pntpbnd1a  27552  pntpbnd1  27553  pntpbnd2  27554  pntibndlem2  27558  pntlemb  27564  pntlemq  27568  pntlemr  27569  pntlemj  27570  pntlemf  27572  pntlemp  27577  ostth2lem2  27601  axpaschlem  29013  axlowdimlem16  29030  smcnlem  30772  bcm1n  32875  sgnmul  32916  wrdt2ind  33035  cycpmco2lem6  33213  cyc3conja  33239  smatrcl  33953  fiunelros  34331  dya2icoseg  34434  eulerpartlemgc  34519  dstfrvunirn  34632  ballotlemfc0  34650  ballotlemfcc  34651  ballotlemimin  34663  ballotlemsgt1  34668  ballotlemfrcn0  34687  fdvposlt  34756  breprexp  34790  logdivsqrle  34807  hgt750leme  34815  tgoldbachgt  34820  lpadmax  34839  lpadright  34841  subfacval3  35383  erdszelem8  35392  cvmliftlem6  35484  cvmliftlem7  35485  cvmliftlem8  35486  cvmliftlem9  35487  cvmliftlem10  35488  sinccvglem  35866  dnibndlem9  36686  unbdqndv2lem2  36710  knoppndvlem14  36725  knoppndvlem18  36729  knoppndvlem19  36730  poimirlem7  37828  poimirlem15  37836  opnmbllem0  37857  itg2addnclem  37872  itg2addnclem3  37874  itg2addnc  37875  itg2gt0cn  37876  areacirclem1  37909  areacirc  37914  isbnd3  37985  cntotbnd  37997  rrnequiv  38036  lcmineqlem11  42293  lcmineqlem22  42304  3lexlogpow5ineq2  42309  3lexlogpow5ineq5  42314  dvrelogpow2b  42322  aks4d1p1p2  42324  aks4d1p1p4  42325  aks4d1p1p6  42327  aks4d1p1p7  42328  aks4d1p1p5  42329  aks4d1p1  42330  aks4d1p2  42331  aks4d1p3  42332  aks4d1p5  42334  aks4d1p7d1  42336  aks4d1p7  42337  aks4d1p8  42341  hashscontpow1  42375  aks6d1c2lem4  42381  aks6d1c5lem2  42392  sticksstones6  42405  sticksstones12a  42411  sticksstones12  42412  aks6d1c7lem1  42434  unitscyglem2  42450  posqsqznn  42591  redvmptabs  42615  readvrec  42617  fltnltalem  42905  irrapxlem3  43066  pellexlem2  43072  pellfundglb  43127  monotuz  43183  monotoddzzfi  43184  acongrep  43222  cvgdvgrat  44554  hashnzfz2  44562  hashnzfzclim  44563  binomcxplemnotnn0  44597  monoords  45545  xralrple2  45599  reclt0d  45631  reclt0  45635  uzublem  45674  cvgcaule  45735  iooiinicc  45788  iooiinioc  45802  limciccioolb  45867  limcicciooub  45881  lptre2pt  45884  limsupubuzlem  45956  limsup10exlem  46016  icccncfext  46131  cncfiooicclem1  46137  dvdivbd  46167  dvbdfbdioolem1  46172  dvbdfbdioolem2  46173  ioodvbdlimc1lem2  46176  ioodvbdlimc2lem  46178  dvnxpaek  46186  dvnmul  46187  volioc  46216  iblspltprt  46217  itgspltprt  46223  volico  46227  volioore  46234  voliooico  46236  voliccico  46243  stoweidlem1  46245  stoweidlem3  46247  stoweidlem7  46251  stoweidlem24  46268  stoweidlem26  46270  stoweidlem42  46286  wallispilem5  46313  stirlinglem1  46318  stirlinglem6  46323  stirlinglem7  46324  stirlinglem10  46327  stirlinglem12  46329  stirlinglem13  46330  stirlingr  46334  dirkertrigeqlem1  46342  fourierdlem10  46361  fourierdlem11  46362  fourierdlem12  46363  fourierdlem14  46365  fourierdlem15  46366  fourierdlem17  46368  fourierdlem19  46370  fourierdlem30  46381  fourierdlem37  46388  fourierdlem40  46391  fourierdlem41  46392  fourierdlem42  46393  fourierdlem47  46397  fourierdlem48  46398  fourierdlem49  46399  fourierdlem50  46400  fourierdlem51  46401  fourierdlem54  46404  fourierdlem63  46413  fourierdlem64  46414  fourierdlem65  46415  fourierdlem68  46418  fourierdlem73  46423  fourierdlem74  46424  fourierdlem76  46426  fourierdlem77  46427  fourierdlem78  46428  fourierdlem79  46429  fourierdlem81  46431  fourierdlem82  46432  fourierdlem83  46433  fourierdlem92  46442  fourierdlem93  46443  fourierdlem102  46452  fourierdlem103  46453  fourierdlem104  46454  fourierdlem107  46457  fourierdlem111  46461  fourierdlem114  46464  sqwvfoura  46472  sqwvfourb  46473  fouriersw  46475  etransclem19  46497  etransclem23  46501  etransclem35  46513  etransclem41  46519  qndenserrnbllem  46538  iundjiun  46704  carageniuncllem2  46766  caratheodorylem1  46770  hoicvr  46792  ovnsubaddlem1  46814  hsphoidmvle2  46829  hoidmv1lelem1  46835  hoidmv1lelem2  46836  hoidmvlelem1  46839  hoidmvlelem2  46840  hoidmvlelem3  46841  hoiqssbllem1  46866  hoiqssbllem2  46867  volico2  46885  iinhoiicclem  46917  iunhoiioolem  46919  vonioolem2  46925  vonicclem2  46928  pimdecfgtioo  46961  pimincfltioo  46962  smflimlem4  47018  smfmullem1  47035  smflimsuplem4  47067  gpg3kgrtriexlem4  48332  gpg3kgrtriexlem6  48334  expnegico01  48764  eenglngeehlnmlem2  48984  inlinecirc02plem  49032