Theorem ltled 11392

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

Syntax hints:   → wi 4   ∈ wcel 2107   class class class wbr 5125  ℝcr 11137   < clt 11278   ≤ cle 11279

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-sep 5278  ax-nul 5288  ax-pow 5347  ax-pr 5414  ax-un 7738  ax-resscn 11195  ax-pre-lttri 11212

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ne 2932  df-nel 3036  df-ral 3051  df-rex 3060  df-rab 3421  df-v 3466  df-sbc 3773  df-csb 3882  df-dif 3936  df-un 3938  df-in 3940  df-ss 3950  df-nul 4316  df-if 4508  df-pw 4584  df-sn 4609  df-pr 4611  df-op 4615  df-uni 4890  df-br 5126  df-opab 5188  df-mpt 5208  df-id 5560  df-xp 5673  df-rel 5674  df-cnv 5675  df-co 5676  df-dm 5677  df-rn 5678  df-res 5679  df-ima 5680  df-iota 6495  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-er 8728  df-en 8969  df-dom 8970  df-sdom 8971  df-pnf 11280  df-mnf 11281  df-xr 11282  df-ltxr 11283  df-le 11284

This theorem is referenced by:  ltnsymd  11393  mulge0  11764  msqge0  11767  addgt0d  11821  lt2addd  11869  lt2msq1  12135  uzwo3  12968  fznatpl1  13601  flflp1  13830  modaddmodup  13958  expmulnbnd  14257  fzsdom2  14450  repswcshw  14833  isercolllem1  15684  caucvgrlem  15692  climcnds  15870  geomulcvg  15895  mertenslem1  15903  ruclem2  16251  ruclem12  16260  bitsfzo  16455  bitsmod  16456  nn0rppwr  16581  nn0expgcd  16584  lcmgcdlem  16626  isprm7  16728  4sqlem7  16965  vdwlem1  17002  met1stc  24497  cfilucfil  24535  nlmvscnlem2  24661  icccmplem2  24800  reconnlem2  24804  xrhmeo  24932  cnheibor  24942  nmoleub2lem3  25103  ipcnlem2  25233  minveclem3b  25417  ivthlem1  25441  ivthlem2  25442  ivth2  25445  ivthle  25446  ivthle2  25447  ovollb2lem  25478  ovolicc2lem4  25510  ovolicc2lem5  25511  ioombl1lem4  25551  uniioombllem4  25576  uniioombllem5  25577  opnmbllem  25591  ismbf3d  25644  mbfi1fseqlem6  25710  itg2gt0  25750  dveflem  25972  dvferm1lem  25977  dvferm2lem  25979  rollelem  25982  rolle  25983  cmvth  25984  cmvthOLD  25985  mvth  25986  c1liplem1  25990  dvgt0lem1  25996  dvivthlem1  26002  lhop1lem  26007  lhop1  26008  dvcnvrelem1  26011  dvcnvrelem2  26012  dvcvx  26014  dgradd2  26263  aaliou3lem8  26342  aaliou3lem7  26346  ulmdvlem1  26398  itgulm  26406  radcnvlt1  26416  radcnvle  26418  abelthlem7  26437  efcvx  26448  coseq0negpitopi  26500  tangtx  26502  tanabsge  26503  tanord  26535  abslogimle  26570  divlogrlim  26632  logno1  26633  logcnlem3  26641  logcnlem4  26642  logtayl  26657  logccv  26660  cxple  26692  rtprmirr  26758  chordthmlem4  26833  asinsin  26890  atanlogaddlem  26911  atantan  26921  cxp2limlem  26974  logdifbnd  26992  emcllem4  26997  harmonicbnd4  27009  lgamucov  27036  ftalem1  27071  ftalem2  27072  ftalem3  27073  basellem5  27083  basellem8  27086  chpchtsum  27218  bposlem1  27283  lgseisenlem1  27374  lgsquadlem1  27379  lgsquadlem2  27380  lgsquadlem3  27381  2sqreulem1  27445  2sqreunnlem1  27448  chebbnd1lem2  27469  chebbnd1lem3  27470  chtppilimlem1  27472  chto1ub  27475  chpo1ubb  27480  vmadivsumb  27482  dchrisumlem3  27490  mulog2sumlem1  27533  vmalogdivsum2  27537  vmalogdivsum  27538  2vmadivsumlem  27539  selbergb  27548  selberg2b  27551  chpdifbndlem1  27552  selberg3lem2  27557  selberg3  27558  selberg4lem1  27559  selberg4  27560  pntrsumbnd  27565  selberg3r  27568  selberg4r  27569  selberg34r  27570  pntrlog2bndlem1  27576  pntrlog2bndlem2  27577  pntrlog2bndlem3  27578  pntrlog2bndlem4  27579  pntrlog2bndlem5  27580  pntrlog2bndlem6a  27581  pntrlog2bndlem6  27582  pntrlog2bnd  27583  pntpbnd1a  27584  pntpbnd1  27585  pntpbnd2  27586  pntibndlem2  27590  pntlemb  27596  pntlemq  27600  pntlemr  27601  pntlemj  27602  pntlemf  27604  pntlemp  27609  ostth2lem2  27633  axpaschlem  28904  axlowdimlem16  28921  smcnlem  30663  bcm1n  32744  wrdt2ind  32885  chnub  32948  cycpmco2lem6  33097  cyc3conja  33123  smatrcl  33736  fiunelros  34116  dya2icoseg  34220  eulerpartlemgc  34305  dstfrvunirn  34418  ballotlemfc0  34436  ballotlemfcc  34437  ballotlemimin  34449  ballotlemsgt1  34454  ballotlemfrcn0  34473  sgnmul  34486  fdvposlt  34555  breprexp  34589  logdivsqrle  34606  hgt750leme  34614  tgoldbachgt  34619  lpadmax  34638  lpadright  34640  subfacval3  35135  erdszelem8  35144  cvmliftlem6  35236  cvmliftlem7  35237  cvmliftlem8  35238  cvmliftlem9  35239  cvmliftlem10  35240  sinccvglem  35618  dnibndlem9  36428  unbdqndv2lem2  36452  knoppndvlem14  36467  knoppndvlem18  36471  knoppndvlem19  36472  poimirlem7  37575  poimirlem15  37583  opnmbllem0  37604  itg2addnclem  37619  itg2addnclem3  37621  itg2addnc  37622  itg2gt0cn  37623  areacirclem1  37656  areacirc  37661  isbnd3  37732  cntotbnd  37744  rrnequiv  37783  lcmineqlem11  41981  lcmineqlem22  41992  3lexlogpow5ineq2  41997  3lexlogpow5ineq5  42002  dvrelogpow2b  42010  aks4d1p1p2  42012  aks4d1p1p4  42013  aks4d1p1p6  42015  aks4d1p1p7  42016  aks4d1p1p5  42017  aks4d1p1  42018  aks4d1p2  42019  aks4d1p3  42020  aks4d1p5  42022  aks4d1p7d1  42024  aks4d1p7  42025  aks4d1p8  42029  hashscontpow1  42063  aks6d1c2lem4  42069  aks6d1c5lem2  42080  sticksstones6  42093  sticksstones12a  42099  sticksstones12  42100  aks6d1c7lem1  42122  unitscyglem2  42138  metakunt7  42153  metakunt29  42175  metakunt30  42176  posqsqznn  42316  redvmptabs  42335  readvrec  42337  fltnltalem  42617  irrapxlem3  42780  pellexlem2  42786  pellfundglb  42841  monotuz  42898  monotoddzzfi  42899  acongrep  42937  cvgdvgrat  44277  hashnzfz2  44285  hashnzfzclim  44286  binomcxplemnotnn0  44320  monoords  45254  xralrple2  45310  reclt0d  45343  reclt0  45347  uzublem  45386  cvgcaule  45447  iooiinicc  45500  iooiinioc  45514  limciccioolb  45581  limcicciooub  45597  lptre2pt  45600  limsupubuzlem  45672  limsup10exlem  45732  icccncfext  45847  cncfiooicclem1  45853  dvdivbd  45883  dvbdfbdioolem1  45888  dvbdfbdioolem2  45889  ioodvbdlimc1lem2  45892  ioodvbdlimc2lem  45894  dvnxpaek  45902  dvnmul  45903  volioc  45932  iblspltprt  45933  itgspltprt  45939  volico  45943  volioore  45950  voliooico  45952  voliccico  45959  stoweidlem1  45961  stoweidlem3  45963  stoweidlem7  45967  stoweidlem24  45984  stoweidlem26  45986  stoweidlem42  46002  wallispilem5  46029  stirlinglem1  46034  stirlinglem6  46039  stirlinglem7  46040  stirlinglem10  46043  stirlinglem12  46045  stirlinglem13  46046  stirlingr  46050  dirkertrigeqlem1  46058  fourierdlem10  46077  fourierdlem11  46078  fourierdlem12  46079  fourierdlem14  46081  fourierdlem15  46082  fourierdlem17  46084  fourierdlem19  46086  fourierdlem30  46097  fourierdlem37  46104  fourierdlem40  46107  fourierdlem41  46108  fourierdlem42  46109  fourierdlem47  46113  fourierdlem48  46114  fourierdlem49  46115  fourierdlem50  46116  fourierdlem51  46117  fourierdlem54  46120  fourierdlem63  46129  fourierdlem64  46130  fourierdlem65  46131  fourierdlem68  46134  fourierdlem73  46139  fourierdlem74  46140  fourierdlem76  46142  fourierdlem77  46143  fourierdlem78  46144  fourierdlem79  46145  fourierdlem81  46147  fourierdlem82  46148  fourierdlem83  46149  fourierdlem92  46158  fourierdlem93  46159  fourierdlem102  46168  fourierdlem103  46169  fourierdlem104  46170  fourierdlem107  46173  fourierdlem111  46177  fourierdlem114  46180  sqwvfoura  46188  sqwvfourb  46189  fouriersw  46191  etransclem19  46213  etransclem23  46217  etransclem35  46229  etransclem41  46235  qndenserrnbllem  46254  iundjiun  46420  carageniuncllem2  46482  caratheodorylem1  46486  hoicvr  46508  ovnsubaddlem1  46530  hsphoidmvle2  46545  hoidmv1lelem1  46551  hoidmv1lelem2  46552  hoidmvlelem1  46555  hoidmvlelem2  46556  hoidmvlelem3  46557  hoiqssbllem1  46582  hoiqssbllem2  46583  volico2  46601  iinhoiicclem  46633  iunhoiioolem  46635  vonioolem2  46641  vonicclem2  46644  pimdecfgtioo  46677  pimincfltioo  46678  smflimlem4  46734  smfmullem1  46751  smflimsuplem4  46783  gpg3kgrtriexlem4  47988  gpg3kgrtriexlem6  47990  expnegico01  48381  eenglngeehlnmlem2  48605  inlinecirc02plem  48653