Theorem ltled 11462

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144   class class class wbr 5102  ℝcr 11203   < clt 11347   ≤ cle 11348

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7752  ax-resscn 11261  ax-pre-lttri 11278

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-iota 6494  df-fun 6541  df-fn 6542  df-f 6543  df-f1 6544  df-fo 6545  df-f1o 6546  df-fv 6547  df-er 8721  df-en 8978  df-dom 8979  df-sdom 8980  df-pnf 11349  df-mnf 11350  df-xr 11351  df-ltxr 11352  df-le 11353

This theorem is used by:  ltnsymd  11463  mulge0  11838  msqge0  11841  addgt0d  11895  lt2addd  11943  lt2msq1  12205  uzwo3  13074  fznatpl1  13716  flflp1  13951  modaddmodup  14081  expmulnbnd  14383  fzsdom2  14577  repswcshw  14968  sgnmul  15266  isercolllem1  15838  caucvgrlem  15846  climcnds  16026  geomulcvg  16051  mertenslem1  16059  ruclem2  16406  ruclem12  16415  bitsfzo  16611  bitsmod  16612  nn0rppwr  16741  nn0expgcd  16744  lcmgcdlem  16787  isprm7  16890  posqsqznn  16942  4sqlem7  17128  vdwlem1  17165  chnub  18802  met1stc  24846  cfilucfil  24884  nlmvscnlem2  25010  icccmplem2  25149  reconnlem2  25153  xrhmeo  25273  cnheibor  25282  nmoleub2lem3  25442  ipcnlem2  25571  minveclem3b  25755  ivthlem1  25778  ivthlem2  25779  ivth2  25782  ivthle  25783  ivthle2  25784  ovollb2lem  25815  ovolicc2lem4  25847  ovolicc2lem5  25848  ioombl1lem4  25888  uniioombllem4  25913  uniioombllem5  25914  opnmbllem  25928  ismbf3d  25981  mbfi1fseqlem6  26047  itg2gt0  26087  dveflem  26305  dvferm1lem  26310  dvferm2lem  26312  rollelem  26315  rolle  26316  cmvth  26317  mvth  26318  c1liplem1  26322  dvgt0lem1  26328  dvivthlem1  26334  lhop1lem  26339  lhop1  26340  dvcnvrelem1  26343  dvcnvrelem2  26344  dvcvx  26346  dgradd2  26593  aaliou3lem8  26678  aaliou3lem7  26682  ulmdvlem1  26733  itgulm  26741  radcnvlt1  26751  radcnvle  26753  abelthlem7  26771  efcvx  26782  coseq0negpitopi  26838  tangtx  26840  tanabsge  26841  tanord  26872  abslogimle  26907  divlogrlim  26969  logno1  26970  logcnlem3  26978  logcnlem4  26979  logtayl  26994  logccv  26997  cxple  27029  rtprmirr  27094  chordthmlem4  27169  asinsin  27226  atanlogaddlem  27247  atantan  27257  cxp2limlem  27309  logdifbnd  27327  emcllem4  27332  harmonicbnd4  27344  lgamucov  27371  ftalem1  27406  ftalem2  27407  ftalem3  27408  basellem5  27418  basellem8  27421  chpchtsum  27552  bposlem1  27617  lgseisenlem1  27708  lgsquadlem1  27713  lgsquadlem2  27714  lgsquadlem3  27715  2sqreulem1  27779  2sqreunnlem1  27782  chebbnd1lem2  27803  chebbnd1lem3  27804  chtppilimlem1  27806  chto1ub  27809  chpo1ubb  27814  vmadivsumb  27816  dchrisumlem3  27824  mulog2sumlem1  27867  vmalogdivsum2  27871  vmalogdivsum  27872  2vmadivsumlem  27873  selbergb  27882  selberg2b  27885  chpdifbndlem1  27886  selberg3lem2  27891  selberg3  27892  selberg4lem1  27893  selberg4  27894  pntrsumbnd  27899  selberg3r  27902  selberg4r  27903  selberg34r  27904  pntrlog2bndlem1  27910  pntrlog2bndlem2  27911  pntrlog2bndlem3  27912  pntrlog2bndlem4  27913  pntrlog2bndlem5  27914  pntrlog2bndlem6a  27915  pntrlog2bndlem6  27916  pntrlog2bnd  27917  pntpbnd1a  27918  pntpbnd1  27919  pntpbnd2  27920  pntibndlem2  27924  pntlemb  27930  pntlemq  27934  pntlemr  27935  pntlemj  27936  pntlemf  27938  pntlemp  27943  ostth2lem2  27967  axpaschlem  29524  axlowdimlem16  29541  smcnlem  31305  bcm1n  33434  wrdt2ind  33563  cycpmco2lem6  33739  cyc3conja  33765  smatrcl  34475  fiunelros  34854  dya2icoseg  34956  eulerpartlemgc  35041  dstfrvunirn  35154  ballotlemfc0  35172  ballotlemfcc  35173  ballotlemimin  35185  ballotlemsgt1  35190  ballotlemfrcn0  35209  fdvposlt  35275  breprexp  35309  logdivsqrle  35326  hgt750leme  35334  tgoldbachgt  35339  lpadmax  35361  lpadright  35363  subfacval3  36041  erdszelem8  36050  cvmliftlem6  36142  cvmliftlem7  36143  cvmliftlem8  36144  cvmliftlem9  36145  cvmliftlem10  36146  sinccvglem  36524  dnibndlem9  37445  unbdqndv2lem2  37469  knoppndvlem14  37484  knoppndvlem18  37488  knoppndvlem19  37489  poimirlem7  38639  poimirlem15  38647  opnmbllem0  38668  itg2addnclem  38683  itg2addnclem3  38685  itg2addnc  38686  itg2gt0cn  38687  areacirclem1  38720  areacirc  38725  isbnd3  38812  cntotbnd  38824  rrnequiv  38863  lcmineqlem11  43183  lcmineqlem22  43194  3lexlogpow5ineq2  43199  3lexlogpow5ineq5  43204  dvrelogpow2b  43212  aks4d1p1p2  43214  aks4d1p1p4  43215  aks4d1p1p6  43217  aks4d1p1p7  43218  aks4d1p1p5  43219  aks4d1p1  43220  aks4d1p2  43221  aks4d1p3  43222  aks4d1p5  43224  aks4d1p7d1  43226  aks4d1p7  43227  aks4d1p8  43231  hashscontpow1  43265  aks6d1c2lem4  43271  aks6d1c5lem2  43282  sticksstones6  43295  sticksstones12a  43301  sticksstones12  43302  aks6d1c7lem1  43324  unitscyglem2  43340  redvmptabs  43505  readvrec  43507  fltnltalem  43767  irrapxlem3  43925  pellexlem2  43931  pellfundglb  43986  monotuz  44042  monotoddzzfi  44043  acongrep  44081  cvgdvgrat  45391  hashnzfz2  45399  hashnzfzclim  45400  binomcxplemnotnn0  45434  monoords  46407  xralrple2  46460  reclt0d  46492  reclt0  46496  uzublem  46534  cvgcaule  46595  iooiinicc  46648  iooiinioc  46662  limciccioolb  46727  limcicciooub  46741  lptre2pt  46744  limsupubuzlem  46816  limsup10exlem  46876  icccncfext  46991  cncfiooicclem1  46997  dvdivbd  47027  dvbdfbdioolem1  47032  dvbdfbdioolem2  47033  ioodvbdlimc1lem2  47036  ioodvbdlimc2lem  47038  dvnxpaek  47046  dvnmul  47047  volioc  47076  iblspltprt  47077  itgspltprt  47083  volico  47087  volioore  47094  voliooico  47096  voliccico  47103  stoweidlem1  47105  stoweidlem3  47107  stoweidlem7  47111  stoweidlem24  47128  stoweidlem26  47130  stoweidlem42  47146  wallispilem5  47173  stirlinglem1  47178  stirlinglem6  47183  stirlinglem7  47184  stirlinglem10  47187  stirlinglem12  47189  stirlinglem13  47190  stirlingr  47194  dirkertrigeqlem1  47202  fourierdlem10  47221  fourierdlem11  47222  fourierdlem12  47223  fourierdlem14  47225  fourierdlem15  47226  fourierdlem17  47228  fourierdlem19  47230  fourierdlem30  47241  fourierdlem37  47248  fourierdlem40  47251  fourierdlem41  47252  fourierdlem42  47253  fourierdlem47  47257  fourierdlem48  47258  fourierdlem49  47259  fourierdlem50  47260  fourierdlem51  47261  fourierdlem54  47264  fourierdlem63  47273  fourierdlem64  47274  fourierdlem65  47275  fourierdlem68  47278  fourierdlem73  47283  fourierdlem74  47284  fourierdlem76  47286  fourierdlem77  47287  fourierdlem78  47288  fourierdlem79  47289  fourierdlem81  47291  fourierdlem82  47292  fourierdlem83  47293  fourierdlem92  47302  fourierdlem93  47303  fourierdlem102  47312  fourierdlem103  47313  fourierdlem104  47314  fourierdlem107  47317  fourierdlem111  47321  fourierdlem114  47324  sqwvfoura  47332  sqwvfourb  47333  fouriersw  47335  etransclem19  47357  etransclem23  47361  etransclem35  47373  etransclem41  47379  qndenserrnbllem  47398  iundjiun  47564  carageniuncllem2  47626  caratheodorylem1  47630  hoicvr  47652  ovnsubaddlem1  47674  hsphoidmvle2  47689  hoidmv1lelem1  47695  hoidmv1lelem2  47696  hoidmvlelem1  47699  hoidmvlelem2  47700  hoidmvlelem3  47701  hoiqssbllem1  47726  hoiqssbllem2  47727  volico2  47745  iinhoiicclem  47777  iunhoiioolem  47779  vonioolem2  47785  vonicclem2  47788  pimdecfgtioo  47821  pimincfltioo  47822  smflimlem4  47878  smfmullem1  47895  smflimsuplem4  47927  gpg3kgrtriexlem4  49278  gpg3kgrtriexlem6  49280  expnegico01  49724  eenglngeehlnmlem2  49945  inlinecirc02plem  49992