Theorem ltled 10782

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

Syntax hints:   → wi 4   ∈ wcel 2110   class class class wbr 5059  ℝcr 10530   < clt 10669   ≤ cle 10670

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793  ax-sep 5196  ax-nul 5203  ax-pow 5259  ax-pr 5322  ax-un 7455  ax-resscn 10588  ax-pre-lttri 10605

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3497  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4833  df-br 5060  df-opab 5122  df-mpt 5140  df-id 5455  df-xp 5556  df-rel 5557  df-cnv 5558  df-co 5559  df-dm 5560  df-rn 5561  df-res 5562  df-ima 5563  df-iota 6309  df-fun 6352  df-fn 6353  df-f 6354  df-f1 6355  df-fo 6356  df-f1o 6357  df-fv 6358  df-er 8283  df-en 8504  df-dom 8505  df-sdom 8506  df-pnf 10671  df-mnf 10672  df-xr 10673  df-ltxr 10674  df-le 10675

This theorem is referenced by:  ltnsymd  10783  mulge0  11152  msqge0  11155  addgt0d  11209  lt2addd  11257  lt2msq1  11518  uzwo3  12337  fznatpl1  12955  flflp1  13171  modaddmodup  13296  expmulnbnd  13590  fzsdom2  13783  repswcshw  14168  isercolllem1  15015  caucvgrlem  15023  climcnds  15200  geomulcvg  15226  mertenslem1  15234  ruclem2  15579  ruclem12  15588  bitsfzo  15778  bitsmod  15779  lcmgcdlem  15944  isprm7  16046  4sqlem7  16274  vdwlem1  16311  met1stc  23125  cfilucfil  23163  nlmvscnlem2  23288  icccmplem2  23425  reconnlem2  23429  xrhmeo  23544  cnheibor  23553  nmoleub2lem3  23713  ipcnlem2  23841  minveclem3b  24025  ivthlem1  24046  ivthlem2  24047  ivth2  24050  ivthle  24051  ivthle2  24052  ovollb2lem  24083  ovolicc2lem4  24115  ovolicc2lem5  24116  ioombl1lem4  24156  uniioombllem4  24181  uniioombllem5  24182  opnmbllem  24196  ismbf3d  24249  mbfi1fseqlem6  24315  itg2gt0  24355  dveflem  24570  dvferm1lem  24575  dvferm2lem  24577  rollelem  24580  rolle  24581  cmvth  24582  mvth  24583  c1liplem1  24587  dvgt0lem1  24593  dvivthlem1  24599  lhop1lem  24604  lhop1  24605  dvcnvrelem1  24608  dvcnvrelem2  24609  dvcvx  24611  dgradd2  24852  aaliou3lem8  24928  aaliou3lem7  24932  ulmdvlem1  24982  itgulm  24990  radcnvlt1  25000  radcnvle  25002  abelthlem7  25020  efcvx  25031  coseq0negpitopi  25083  tangtx  25085  tanabsge  25086  tanord  25116  abslogimle  25151  divlogrlim  25212  logno1  25213  logcnlem3  25221  logcnlem4  25222  logtayl  25237  logccv  25240  cxple  25272  chordthmlem4  25407  asinsin  25464  atanlogaddlem  25485  atantan  25495  cxp2limlem  25547  logdifbnd  25565  emcllem4  25570  harmonicbnd4  25582  lgamucov  25609  ftalem1  25644  ftalem2  25645  ftalem3  25646  basellem5  25656  basellem8  25659  chpchtsum  25789  bposlem1  25854  lgseisenlem1  25945  lgsquadlem1  25950  lgsquadlem2  25951  lgsquadlem3  25952  2sqreulem1  26016  2sqreunnlem1  26019  chebbnd1lem2  26040  chebbnd1lem3  26041  chtppilimlem1  26043  chto1ub  26046  chpo1ubb  26051  vmadivsumb  26053  dchrisumlem3  26061  mulog2sumlem1  26104  vmalogdivsum2  26108  vmalogdivsum  26109  2vmadivsumlem  26110  selbergb  26119  selberg2b  26122  chpdifbndlem1  26123  selberg3lem2  26128  selberg3  26129  selberg4lem1  26130  selberg4  26131  pntrsumbnd  26136  selberg3r  26139  selberg4r  26140  selberg34r  26141  pntrlog2bndlem1  26147  pntrlog2bndlem2  26148  pntrlog2bndlem3  26149  pntrlog2bndlem4  26150  pntrlog2bndlem5  26151  pntrlog2bndlem6a  26152  pntrlog2bndlem6  26153  pntrlog2bnd  26154  pntpbnd1a  26155  pntpbnd1  26156  pntpbnd2  26157  pntibndlem2  26161  pntlemb  26167  pntlemq  26171  pntlemr  26172  pntlemj  26173  pntlemf  26175  pntlemp  26180  ostth2lem2  26204  axpaschlem  26720  axlowdimlem16  26737  smcnlem  28468  bcm1n  30512  wrdt2ind  30622  cycpmco2lem6  30768  cyc3conja  30794  smatrcl  31056  fiunelros  31428  dya2icoseg  31530  eulerpartlemgc  31615  dstfrvunirn  31727  ballotlemfc0  31745  ballotlemfcc  31746  ballotlemimin  31758  ballotlemsgt1  31763  ballotlemfrcn0  31782  sgnmul  31795  fdvposlt  31865  breprexp  31899  logdivsqrle  31916  hgt750leme  31924  tgoldbachgt  31929  lpadmax  31948  lpadright  31950  subfacval3  32431  erdszelem8  32440  cvmliftlem6  32532  cvmliftlem7  32533  cvmliftlem8  32534  cvmliftlem9  32535  cvmliftlem10  32536  sinccvglem  32910  dnibndlem9  33820  unbdqndv2lem2  33844  knoppndvlem14  33859  knoppndvlem18  33863  knoppndvlem19  33864  poimirlem7  34893  poimirlem15  34901  opnmbllem0  34922  itg2addnclem  34937  itg2addnclem3  34939  itg2addnc  34940  itg2gt0cn  34941  areacirclem1  34976  areacirc  34981  isbnd3  35056  cntotbnd  35068  rrnequiv  35107  nn0rppwr  39175  nn0expgcd  39177  rtprmirr  39187  fltnltalem  39267  irrapxlem3  39414  pellexlem2  39420  pellfundglb  39475  monotuz  39531  monotoddzzfi  39532  acongrep  39570  cvgdvgrat  40638  hashnzfz2  40646  hashnzfzclim  40647  binomcxplemnotnn0  40681  monoords  41556  xralrple2  41614  reclt0d  41650  reclt0  41655  uzublem  41696  iooiinicc  41810  iooiinioc  41824  limciccioolb  41894  limcicciooub  41910  lptre2pt  41913  limsupubuzlem  41985  limsup10exlem  42045  icccncfext  42162  cncfiooicclem1  42168  dvdivbd  42200  dvbdfbdioolem1  42205  dvbdfbdioolem2  42206  ioodvbdlimc1lem2  42209  ioodvbdlimc2lem  42211  dvnxpaek  42219  dvnmul  42220  volioc  42249  iblspltprt  42250  itgspltprt  42256  volico  42261  volioore  42268  voliooico  42270  voliccico  42277  stoweidlem1  42279  stoweidlem3  42281  stoweidlem7  42285  stoweidlem24  42302  stoweidlem26  42304  stoweidlem42  42320  wallispilem5  42347  stirlinglem1  42352  stirlinglem6  42357  stirlinglem7  42358  stirlinglem10  42361  stirlinglem12  42363  stirlinglem13  42364  stirlingr  42368  dirkertrigeqlem1  42376  fourierdlem10  42395  fourierdlem11  42396  fourierdlem12  42397  fourierdlem14  42399  fourierdlem15  42400  fourierdlem17  42402  fourierdlem19  42404  fourierdlem30  42415  fourierdlem37  42422  fourierdlem40  42425  fourierdlem41  42426  fourierdlem42  42427  fourierdlem47  42431  fourierdlem48  42432  fourierdlem49  42433  fourierdlem50  42434  fourierdlem51  42435  fourierdlem54  42438  fourierdlem63  42447  fourierdlem64  42448  fourierdlem65  42449  fourierdlem68  42452  fourierdlem73  42457  fourierdlem74  42458  fourierdlem76  42460  fourierdlem77  42461  fourierdlem78  42462  fourierdlem79  42463  fourierdlem81  42465  fourierdlem82  42466  fourierdlem83  42467  fourierdlem92  42476  fourierdlem93  42477  fourierdlem102  42486  fourierdlem103  42487  fourierdlem104  42488  fourierdlem107  42491  fourierdlem111  42495  fourierdlem114  42498  sqwvfoura  42506  sqwvfourb  42507  fouriersw  42509  etransclem19  42531  etransclem23  42535  etransclem35  42547  etransclem41  42553  qndenserrnbllem  42572  iundjiun  42735  carageniuncllem2  42797  caratheodorylem1  42801  hoicvr  42823  ovnsubaddlem1  42845  hsphoidmvle2  42860  hoidmv1lelem1  42866  hoidmv1lelem2  42867  hoidmvlelem1  42870  hoidmvlelem2  42871  hoidmvlelem3  42872  hoiqssbllem1  42897  hoiqssbllem2  42898  volico2  42916  iinhoiicclem  42948  iunhoiioolem  42950  vonioolem2  42956  vonicclem2  42959  pimdecfgtioo  42988  pimincfltioo  42989  smflimlem4  43043  smfmullem1  43059  smflimsuplem4  43090  expnegico01  44566  eenglngeehlnmlem2  44718  inlinecirc02plem  44766