Theorem ltled 11366

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

Syntax hints:   → wi 4   ∈ wcel 2104   class class class wbr 5147  ℝcr 11111   < clt 11252   ≤ cle 11253

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 2701  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727  ax-resscn 11169  ax-pre-lttri 11186

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-er 8705  df-en 8942  df-dom 8943  df-sdom 8944  df-pnf 11254  df-mnf 11255  df-xr 11256  df-ltxr 11257  df-le 11258

This theorem is referenced by:  ltnsymd  11367  mulge0  11736  msqge0  11739  addgt0d  11793  lt2addd  11841  lt2msq1  12102  uzwo3  12931  fznatpl1  13559  flflp1  13776  modaddmodup  13903  expmulnbnd  14202  fzsdom2  14392  repswcshw  14766  isercolllem1  15615  caucvgrlem  15623  climcnds  15801  geomulcvg  15826  mertenslem1  15834  ruclem2  16179  ruclem12  16188  bitsfzo  16380  bitsmod  16381  lcmgcdlem  16547  isprm7  16649  4sqlem7  16881  vdwlem1  16918  met1stc  24250  cfilucfil  24288  nlmvscnlem2  24422  icccmplem2  24559  reconnlem2  24563  xrhmeo  24691  cnheibor  24701  nmoleub2lem3  24862  ipcnlem2  24992  minveclem3b  25176  ivthlem1  25200  ivthlem2  25201  ivth2  25204  ivthle  25205  ivthle2  25206  ovollb2lem  25237  ovolicc2lem4  25269  ovolicc2lem5  25270  ioombl1lem4  25310  uniioombllem4  25335  uniioombllem5  25336  opnmbllem  25350  ismbf3d  25403  mbfi1fseqlem6  25470  itg2gt0  25510  dveflem  25731  dvferm1lem  25736  dvferm2lem  25738  rollelem  25741  rolle  25742  cmvth  25743  mvth  25744  c1liplem1  25748  dvgt0lem1  25754  dvivthlem1  25760  lhop1lem  25765  lhop1  25766  dvcnvrelem1  25769  dvcnvrelem2  25770  dvcvx  25772  dgradd2  26018  aaliou3lem8  26094  aaliou3lem7  26098  ulmdvlem1  26148  itgulm  26156  radcnvlt1  26166  radcnvle  26168  abelthlem7  26186  efcvx  26197  coseq0negpitopi  26249  tangtx  26251  tanabsge  26252  tanord  26283  abslogimle  26318  divlogrlim  26379  logno1  26380  logcnlem3  26388  logcnlem4  26389  logtayl  26404  logccv  26407  cxple  26439  chordthmlem4  26576  asinsin  26633  atanlogaddlem  26654  atantan  26664  cxp2limlem  26716  logdifbnd  26734  emcllem4  26739  harmonicbnd4  26751  lgamucov  26778  ftalem1  26813  ftalem2  26814  ftalem3  26815  basellem5  26825  basellem8  26828  chpchtsum  26958  bposlem1  27023  lgseisenlem1  27114  lgsquadlem1  27119  lgsquadlem2  27120  lgsquadlem3  27121  2sqreulem1  27185  2sqreunnlem1  27188  chebbnd1lem2  27209  chebbnd1lem3  27210  chtppilimlem1  27212  chto1ub  27215  chpo1ubb  27220  vmadivsumb  27222  dchrisumlem3  27230  mulog2sumlem1  27273  vmalogdivsum2  27277  vmalogdivsum  27278  2vmadivsumlem  27279  selbergb  27288  selberg2b  27291  chpdifbndlem1  27292  selberg3lem2  27297  selberg3  27298  selberg4lem1  27299  selberg4  27300  pntrsumbnd  27305  selberg3r  27308  selberg4r  27309  selberg34r  27310  pntrlog2bndlem1  27316  pntrlog2bndlem2  27317  pntrlog2bndlem3  27318  pntrlog2bndlem4  27319  pntrlog2bndlem5  27320  pntrlog2bndlem6a  27321  pntrlog2bndlem6  27322  pntrlog2bnd  27323  pntpbnd1a  27324  pntpbnd1  27325  pntpbnd2  27326  pntibndlem2  27330  pntlemb  27336  pntlemq  27340  pntlemr  27341  pntlemj  27342  pntlemf  27344  pntlemp  27349  ostth2lem2  27373  axpaschlem  28465  axlowdimlem16  28482  smcnlem  30217  bcm1n  32273  wrdt2ind  32384  cycpmco2lem6  32560  cyc3conja  32586  smatrcl  33074  fiunelros  33470  dya2icoseg  33574  eulerpartlemgc  33659  dstfrvunirn  33771  ballotlemfc0  33789  ballotlemfcc  33790  ballotlemimin  33802  ballotlemsgt1  33807  ballotlemfrcn0  33826  sgnmul  33839  fdvposlt  33909  breprexp  33943  logdivsqrle  33960  hgt750leme  33968  tgoldbachgt  33973  lpadmax  33992  lpadright  33994  subfacval3  34478  erdszelem8  34487  cvmliftlem6  34579  cvmliftlem7  34580  cvmliftlem8  34581  cvmliftlem9  34582  cvmliftlem10  34583  sinccvglem  34955  gg-cmvth  35466  dnibndlem9  35665  unbdqndv2lem2  35689  knoppndvlem14  35704  knoppndvlem18  35708  knoppndvlem19  35709  poimirlem7  36798  poimirlem15  36806  opnmbllem0  36827  itg2addnclem  36842  itg2addnclem3  36844  itg2addnc  36845  itg2gt0cn  36846  areacirclem1  36879  areacirc  36884  isbnd3  36955  cntotbnd  36967  rrnequiv  37006  lcmineqlem11  41210  lcmineqlem22  41221  3lexlogpow5ineq2  41226  3lexlogpow5ineq5  41231  dvrelogpow2b  41239  aks4d1p1p2  41241  aks4d1p1p4  41242  aks4d1p1p6  41244  aks4d1p1p7  41245  aks4d1p1p5  41246  aks4d1p1  41247  aks4d1p2  41248  aks4d1p3  41249  aks4d1p5  41251  aks4d1p7d1  41253  aks4d1p7  41254  aks4d1p8  41258  sticksstones6  41273  sticksstones12a  41279  sticksstones12  41280  metakunt7  41297  metakunt29  41319  metakunt30  41320  nn0rppwr  41526  nn0expgcd  41528  posqsqznn  41536  rtprmirr  41539  fltnltalem  41706  irrapxlem3  41864  pellexlem2  41870  pellfundglb  41925  monotuz  41982  monotoddzzfi  41983  acongrep  42021  cvgdvgrat  43374  hashnzfz2  43382  hashnzfzclim  43383  binomcxplemnotnn0  43417  monoords  44305  xralrple2  44362  reclt0d  44395  reclt0  44399  uzublem  44438  cvgcaule  44500  iooiinicc  44553  iooiinioc  44567  limciccioolb  44635  limcicciooub  44651  lptre2pt  44654  limsupubuzlem  44726  limsup10exlem  44786  icccncfext  44901  cncfiooicclem1  44907  dvdivbd  44937  dvbdfbdioolem1  44942  dvbdfbdioolem2  44943  ioodvbdlimc1lem2  44946  ioodvbdlimc2lem  44948  dvnxpaek  44956  dvnmul  44957  volioc  44986  iblspltprt  44987  itgspltprt  44993  volico  44997  volioore  45004  voliooico  45006  voliccico  45013  stoweidlem1  45015  stoweidlem3  45017  stoweidlem7  45021  stoweidlem24  45038  stoweidlem26  45040  stoweidlem42  45056  wallispilem5  45083  stirlinglem1  45088  stirlinglem6  45093  stirlinglem7  45094  stirlinglem10  45097  stirlinglem12  45099  stirlinglem13  45100  stirlingr  45104  dirkertrigeqlem1  45112  fourierdlem10  45131  fourierdlem11  45132  fourierdlem12  45133  fourierdlem14  45135  fourierdlem15  45136  fourierdlem17  45138  fourierdlem19  45140  fourierdlem30  45151  fourierdlem37  45158  fourierdlem40  45161  fourierdlem41  45162  fourierdlem42  45163  fourierdlem47  45167  fourierdlem48  45168  fourierdlem49  45169  fourierdlem50  45170  fourierdlem51  45171  fourierdlem54  45174  fourierdlem63  45183  fourierdlem64  45184  fourierdlem65  45185  fourierdlem68  45188  fourierdlem73  45193  fourierdlem74  45194  fourierdlem76  45196  fourierdlem77  45197  fourierdlem78  45198  fourierdlem79  45199  fourierdlem81  45201  fourierdlem82  45202  fourierdlem83  45203  fourierdlem92  45212  fourierdlem93  45213  fourierdlem102  45222  fourierdlem103  45223  fourierdlem104  45224  fourierdlem107  45227  fourierdlem111  45231  fourierdlem114  45234  sqwvfoura  45242  sqwvfourb  45243  fouriersw  45245  etransclem19  45267  etransclem23  45271  etransclem35  45283  etransclem41  45289  qndenserrnbllem  45308  iundjiun  45474  carageniuncllem2  45536  caratheodorylem1  45540  hoicvr  45562  ovnsubaddlem1  45584  hsphoidmvle2  45599  hoidmv1lelem1  45605  hoidmv1lelem2  45606  hoidmvlelem1  45609  hoidmvlelem2  45610  hoidmvlelem3  45611  hoiqssbllem1  45636  hoiqssbllem2  45637  volico2  45655  iinhoiicclem  45687  iunhoiioolem  45689  vonioolem2  45695  vonicclem2  45698  pimdecfgtioo  45731  pimincfltioo  45732  smflimlem4  45788  smfmullem1  45805  smflimsuplem4  45837  expnegico01  47286  eenglngeehlnmlem2  47511  inlinecirc02plem  47559