Theorem ltled 11495

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147   class class class wbr 5106  ℝcr 11236   < clt 11380   ≤ cle 11381

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5253  ax-nul 5264  ax-pow 5332  ax-pr 5396  ax-un 7781  ax-resscn 11294  ax-pre-lttri 11311

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5172  df-mpt 5191  df-id 5551  df-xp 5662  df-rel 5663  df-cnv 5664  df-co 5665  df-dm 5666  df-rn 5667  df-res 5668  df-ima 5669  df-iota 6518  df-fun 6566  df-fn 6567  df-f 6568  df-f1 6569  df-fo 6570  df-f1o 6571  df-fv 6572  df-er 8753  df-en 9010  df-dom 9011  df-sdom 9012  df-pnf 11382  df-mnf 11383  df-xr 11384  df-ltxr 11385  df-le 11386

This theorem is used by:  ltnsymd  11496  mulge0  11872  msqge0  11875  addgt0d  11929  lt2addd  11977  lt2msq1  12239  uzwo3  13108  fznatpl1  13750  flflp1  13985  modaddmodup  14115  expmulnbnd  14418  fzsdom2  14612  repswcshw  15003  sgnmul  15301  isercolllem1  15873  caucvgrlem  15881  climcnds  16061  geomulcvg  16086  mertenslem1  16094  ruclem2  16441  ruclem12  16450  bitsfzo  16646  bitsmod  16647  nn0rppwr  16776  nn0expgcd  16779  lcmgcdlem  16822  isprm7  16925  posqsqznn  16977  4sqlem7  17163  vdwlem1  17200  chnub  18837  met1stc  24884  cfilucfil  24922  nlmvscnlem2  25048  icccmplem2  25187  reconnlem2  25191  xrhmeo  25311  cnheibor  25320  nmoleub2lem3  25480  ipcnlem2  25609  minveclem3b  25793  ivthlem1  25816  ivthlem2  25817  ivth2  25820  ivthle  25821  ivthle2  25822  ovollb2lem  25853  ovolicc2lem4  25885  ovolicc2lem5  25886  ioombl1lem4  25926  uniioombllem4  25951  uniioombllem5  25952  opnmbllem  25966  ismbf3d  26019  mbfi1fseqlem6  26085  itg2gt0  26125  dveflem  26343  dvferm1lem  26348  dvferm2lem  26350  rollelem  26353  rolle  26354  cmvth  26355  mvth  26356  c1liplem1  26360  dvgt0lem1  26366  dvivthlem1  26372  lhop1lem  26377  lhop1  26378  dvcnvrelem1  26381  dvcnvrelem2  26382  dvcvx  26384  dgradd2  26631  aaliou3lem8  26718  aaliou3lem7  26722  ulmdvlem1  26773  itgulm  26781  radcnvlt1  26791  radcnvle  26793  abelthlem7  26811  efcvx  26822  coseq0negpitopi  26878  tangtx  26880  tanabsge  26881  tanord  26912  abslogimle  26947  divlogrlim  27009  logno1  27010  logcnlem3  27018  logcnlem4  27019  logtayl  27034  logccv  27037  cxple  27069  rtprmirr  27134  chordthmlem4  27209  asinsin  27266  atanlogaddlem  27287  atantan  27297  cxp2limlem  27349  logdifbnd  27367  emcllem4  27372  harmonicbnd4  27384  lgamucov  27411  ftalem1  27446  ftalem2  27447  ftalem3  27448  basellem5  27458  basellem8  27461  chpchtsum  27592  bposlem1  27657  lgseisenlem1  27748  lgsquadlem1  27753  lgsquadlem2  27754  lgsquadlem3  27755  2sqreulem1  27819  2sqreunnlem1  27822  chebbnd1lem2  27843  chebbnd1lem3  27844  chtppilimlem1  27846  chto1ub  27849  chpo1ubb  27854  vmadivsumb  27856  dchrisumlem3  27864  mulog2sumlem1  27907  vmalogdivsum2  27911  vmalogdivsum  27912  2vmadivsumlem  27913  selbergb  27922  selberg2b  27925  chpdifbndlem1  27926  selberg3lem2  27931  selberg3  27932  selberg4lem1  27933  selberg4  27934  pntrsumbnd  27939  selberg3r  27942  selberg4r  27943  selberg34r  27944  pntrlog2bndlem1  27950  pntrlog2bndlem2  27951  pntrlog2bndlem3  27952  pntrlog2bndlem4  27953  pntrlog2bndlem5  27954  pntrlog2bndlem6a  27955  pntrlog2bndlem6  27956  pntrlog2bnd  27957  pntpbnd1a  27958  pntpbnd1  27959  pntpbnd2  27960  pntibndlem2  27964  pntlemb  27970  pntlemq  27974  pntlemr  27975  pntlemj  27976  pntlemf  27978  pntlemp  27983  ostth2lem2  28007  axpaschlem  29564  axlowdimlem16  29581  smcnlem  31345  bcm1n  33473  wrdt2ind  33602  cycpmco2lem6  33781  cyc3conja  33807  smatrcl  34532  fiunelros  34911  dya2icoseg  35013  eulerpartlemgc  35098  dstfrvunirn  35211  ballotlemfc0  35229  ballotlemfcc  35230  ballotlemimin  35242  ballotlemsgt1  35247  ballotlemfrcn0  35266  fdvposlt  35332  breprexp  35366  logdivsqrle  35383  hgt750leme  35391  tgoldbachgt  35396  lpadmax  35418  lpadright  35420  subfacval3  36155  erdszelem8  36164  cvmliftlem6  36256  cvmliftlem7  36257  cvmliftlem8  36258  cvmliftlem9  36259  cvmliftlem10  36260  sinccvglem  36638  dnibndlem9  37560  unbdqndv2lem2  37584  knoppndvlem14  37599  knoppndvlem18  37603  knoppndvlem19  37604  poimirlem7  38806  poimirlem15  38814  opnmbllem0  38835  itg2addnclem  38850  itg2addnclem3  38852  itg2addnc  38853  itg2gt0cn  38854  areacirclem1  38887  areacirc  38892  isbnd3  38977  cntotbnd  38989  rrnequiv  39028  lcmineqlem11  43348  lcmineqlem22  43359  3lexlogpow5ineq2  43364  3lexlogpow5ineq5  43369  dvrelogpow2b  43377  aks4d1p1p2  43379  aks4d1p1p4  43380  aks4d1p1p6  43382  aks4d1p1p7  43383  aks4d1p1p5  43384  aks4d1p1  43385  aks4d1p2  43386  aks4d1p3  43387  aks4d1p5  43389  aks4d1p7d1  43391  aks4d1p7  43392  aks4d1p8  43396  hashscontpow1  43430  aks6d1c2lem4  43436  aks6d1c5lem2  43447  sticksstones6  43460  sticksstones12a  43466  sticksstones12  43467  aks6d1c7lem1  43489  unitscyglem2  43505  redvmptabs  43671  readvrec  43673  fltnltalem  43933  irrapxlem3  44091  pellexlem2  44097  pellfundglb  44152  monotuz  44208  monotoddzzfi  44209  acongrep  44247  cvgdvgrat  45552  hashnzfz2  45560  hashnzfzclim  45561  binomcxplemnotnn0  45595  monoords  46580  xralrple2  46633  reclt0d  46665  reclt0  46669  uzublem  46707  cvgcaule  46768  iooiinicc  46821  iooiinioc  46835  limciccioolb  46900  limcicciooub  46914  lptre2pt  46917  limsupubuzlem  46989  limsup10exlem  47049  icccncfext  47164  cncfiooicclem1  47170  dvdivbd  47200  dvbdfbdioolem1  47205  dvbdfbdioolem2  47206  ioodvbdlimc1lem2  47209  ioodvbdlimc2lem  47211  dvnxpaek  47219  dvnmul  47220  volioc  47249  iblspltprt  47250  itgspltprt  47256  volico  47260  volioore  47267  voliooico  47269  voliccico  47276  stoweidlem1  47278  stoweidlem3  47280  stoweidlem7  47284  stoweidlem24  47301  stoweidlem26  47303  stoweidlem42  47319  wallispilem5  47346  stirlinglem1  47351  stirlinglem6  47356  stirlinglem7  47357  stirlinglem10  47360  stirlinglem12  47362  stirlinglem13  47363  stirlingr  47367  dirkertrigeqlem1  47375  fourierdlem10  47394  fourierdlem11  47395  fourierdlem12  47396  fourierdlem14  47398  fourierdlem15  47399  fourierdlem17  47401  fourierdlem19  47403  fourierdlem30  47414  fourierdlem37  47421  fourierdlem40  47424  fourierdlem41  47425  fourierdlem42  47426  fourierdlem47  47430  fourierdlem48  47431  fourierdlem49  47432  fourierdlem50  47433  fourierdlem51  47434  fourierdlem54  47437  fourierdlem63  47446  fourierdlem64  47447  fourierdlem65  47448  fourierdlem68  47451  fourierdlem73  47456  fourierdlem74  47457  fourierdlem76  47459  fourierdlem77  47460  fourierdlem78  47461  fourierdlem79  47462  fourierdlem81  47464  fourierdlem82  47465  fourierdlem83  47466  fourierdlem92  47475  fourierdlem93  47476  fourierdlem102  47485  fourierdlem103  47486  fourierdlem104  47487  fourierdlem107  47490  fourierdlem111  47494  fourierdlem114  47497  sqwvfoura  47505  sqwvfourb  47506  fouriersw  47508  etransclem19  47530  etransclem23  47534  etransclem35  47546  etransclem41  47552  qndenserrnbllem  47571  iundjiun  47737  carageniuncllem2  47799  caratheodorylem1  47803  hoicvr  47825  ovnsubaddlem1  47847  hsphoidmvle2  47862  hoidmv1lelem1  47868  hoidmv1lelem2  47869  hoidmvlelem1  47872  hoidmvlelem2  47873  hoidmvlelem3  47874  hoiqssbllem1  47899  hoiqssbllem2  47900  volico2  47918  iinhoiicclem  47950  iunhoiioolem  47952  vonioolem2  47958  vonicclem2  47961  pimdecfgtioo  47994  pimincfltioo  47995  smflimlem4  48051  smfmullem1  48068  smflimsuplem4  48100  gpg3kgrtriexlem4  49451  gpg3kgrtriexlem6  49453  expnegico01  49955  eenglngeehlnmlem2  50176  inlinecirc02plem  50223