Theorem ltled 10859

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

Syntax hints:   → wi 4   ∈ wcel 2113   class class class wbr 5027  ℝcr 10607   < clt 10746   ≤ cle 10747

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2161  ax-12 2178  ax-ext 2710  ax-sep 5164  ax-nul 5171  ax-pow 5229  ax-pr 5293  ax-un 7473  ax-resscn 10665  ax-pre-lttri 10682

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ne 2935  df-nel 3039  df-ral 3058  df-rex 3059  df-rab 3062  df-v 3399  df-sbc 3680  df-csb 3789  df-dif 3844  df-un 3846  df-in 3848  df-ss 3858  df-nul 4210  df-if 4412  df-pw 4487  df-sn 4514  df-pr 4516  df-op 4520  df-uni 4794  df-br 5028  df-opab 5090  df-mpt 5108  df-id 5425  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-iota 6291  df-fun 6335  df-fn 6336  df-f 6337  df-f1 6338  df-fo 6339  df-f1o 6340  df-fv 6341  df-er 8313  df-en 8549  df-dom 8550  df-sdom 8551  df-pnf 10748  df-mnf 10749  df-xr 10750  df-ltxr 10751  df-le 10752

This theorem is referenced by:  ltnsymd  10860  mulge0  11229  msqge0  11232  addgt0d  11286  lt2addd  11334  lt2msq1  11595  uzwo3  12418  fznatpl1  13045  flflp1  13261  modaddmodup  13386  expmulnbnd  13681  fzsdom2  13874  repswcshw  14256  isercolllem1  15107  caucvgrlem  15115  climcnds  15292  geomulcvg  15317  mertenslem1  15325  ruclem2  15670  ruclem12  15679  bitsfzo  15871  bitsmod  15872  lcmgcdlem  16040  isprm7  16142  4sqlem7  16373  vdwlem1  16410  met1stc  23267  cfilucfil  23305  nlmvscnlem2  23431  icccmplem2  23568  reconnlem2  23572  xrhmeo  23691  cnheibor  23700  nmoleub2lem3  23860  ipcnlem2  23989  minveclem3b  24173  ivthlem1  24196  ivthlem2  24197  ivth2  24200  ivthle  24201  ivthle2  24202  ovollb2lem  24233  ovolicc2lem4  24265  ovolicc2lem5  24266  ioombl1lem4  24306  uniioombllem4  24331  uniioombllem5  24332  opnmbllem  24346  ismbf3d  24399  mbfi1fseqlem6  24465  itg2gt0  24505  dveflem  24723  dvferm1lem  24728  dvferm2lem  24730  rollelem  24733  rolle  24734  cmvth  24735  mvth  24736  c1liplem1  24740  dvgt0lem1  24746  dvivthlem1  24752  lhop1lem  24757  lhop1  24758  dvcnvrelem1  24761  dvcnvrelem2  24762  dvcvx  24764  dgradd2  25009  aaliou3lem8  25085  aaliou3lem7  25089  ulmdvlem1  25139  itgulm  25147  radcnvlt1  25157  radcnvle  25159  abelthlem7  25177  efcvx  25188  coseq0negpitopi  25240  tangtx  25242  tanabsge  25243  tanord  25274  abslogimle  25309  divlogrlim  25370  logno1  25371  logcnlem3  25379  logcnlem4  25380  logtayl  25395  logccv  25398  cxple  25430  chordthmlem4  25565  asinsin  25622  atanlogaddlem  25643  atantan  25653  cxp2limlem  25705  logdifbnd  25723  emcllem4  25728  harmonicbnd4  25740  lgamucov  25767  ftalem1  25802  ftalem2  25803  ftalem3  25804  basellem5  25814  basellem8  25817  chpchtsum  25947  bposlem1  26012  lgseisenlem1  26103  lgsquadlem1  26108  lgsquadlem2  26109  lgsquadlem3  26110  2sqreulem1  26174  2sqreunnlem1  26177  chebbnd1lem2  26198  chebbnd1lem3  26199  chtppilimlem1  26201  chto1ub  26204  chpo1ubb  26209  vmadivsumb  26211  dchrisumlem3  26219  mulog2sumlem1  26262  vmalogdivsum2  26266  vmalogdivsum  26267  2vmadivsumlem  26268  selbergb  26277  selberg2b  26280  chpdifbndlem1  26281  selberg3lem2  26286  selberg3  26287  selberg4lem1  26288  selberg4  26289  pntrsumbnd  26294  selberg3r  26297  selberg4r  26298  selberg34r  26299  pntrlog2bndlem1  26305  pntrlog2bndlem2  26306  pntrlog2bndlem3  26307  pntrlog2bndlem4  26308  pntrlog2bndlem5  26309  pntrlog2bndlem6a  26310  pntrlog2bndlem6  26311  pntrlog2bnd  26312  pntpbnd1a  26313  pntpbnd1  26314  pntpbnd2  26315  pntibndlem2  26319  pntlemb  26325  pntlemq  26329  pntlemr  26330  pntlemj  26331  pntlemf  26333  pntlemp  26338  ostth2lem2  26362  axpaschlem  26878  axlowdimlem16  26895  smcnlem  28624  bcm1n  30683  wrdt2ind  30792  cycpmco2lem6  30967  cyc3conja  30993  smatrcl  31310  fiunelros  31704  dya2icoseg  31806  eulerpartlemgc  31891  dstfrvunirn  32003  ballotlemfc0  32021  ballotlemfcc  32022  ballotlemimin  32034  ballotlemsgt1  32039  ballotlemfrcn0  32058  sgnmul  32071  fdvposlt  32141  breprexp  32175  logdivsqrle  32192  hgt750leme  32200  tgoldbachgt  32205  lpadmax  32224  lpadright  32226  subfacval3  32714  erdszelem8  32723  cvmliftlem6  32815  cvmliftlem7  32816  cvmliftlem8  32817  cvmliftlem9  32818  cvmliftlem10  32819  sinccvglem  33193  dnibndlem9  34296  unbdqndv2lem2  34320  knoppndvlem14  34335  knoppndvlem18  34339  knoppndvlem19  34340  poimirlem7  35396  poimirlem15  35404  opnmbllem0  35425  itg2addnclem  35440  itg2addnclem3  35442  itg2addnc  35443  itg2gt0cn  35444  areacirclem1  35477  areacirc  35482  isbnd3  35554  cntotbnd  35566  rrnequiv  35605  lcmineqlem11  39656  lcmineqlem22  39667  3lexlogpow5ineq2  39672  3lexlogpow5ineq5  39677  dvrelogpow2b  39684  aks4d1p1p2  39686  aks4d1p1p4  39687  aks4d1p1p6  39689  aks4d1p1p7  39690  aks4d1p1p5  39691  aks4d1p1  39692  sticksstones6  39702  metakunt7  39711  metakunt29  39733  metakunt30  39734  nn0rppwr  39894  nn0expgcd  39896  posqsqznn  39904  rtprmirr  39908  fltnltalem  40055  irrapxlem3  40202  pellexlem2  40208  pellfundglb  40263  monotuz  40319  monotoddzzfi  40320  acongrep  40358  cvgdvgrat  41453  hashnzfz2  41461  hashnzfzclim  41462  binomcxplemnotnn0  41496  monoords  42358  xralrple2  42415  reclt0d  42448  reclt0  42453  uzublem  42492  iooiinicc  42604  iooiinioc  42618  limciccioolb  42688  limcicciooub  42704  lptre2pt  42707  limsupubuzlem  42779  limsup10exlem  42839  icccncfext  42954  cncfiooicclem1  42960  dvdivbd  42990  dvbdfbdioolem1  42995  dvbdfbdioolem2  42996  ioodvbdlimc1lem2  42999  ioodvbdlimc2lem  43001  dvnxpaek  43009  dvnmul  43010  volioc  43039  iblspltprt  43040  itgspltprt  43046  volico  43050  volioore  43057  voliooico  43059  voliccico  43066  stoweidlem1  43068  stoweidlem3  43070  stoweidlem7  43074  stoweidlem24  43091  stoweidlem26  43093  stoweidlem42  43109  wallispilem5  43136  stirlinglem1  43141  stirlinglem6  43146  stirlinglem7  43147  stirlinglem10  43150  stirlinglem12  43152  stirlinglem13  43153  stirlingr  43157  dirkertrigeqlem1  43165  fourierdlem10  43184  fourierdlem11  43185  fourierdlem12  43186  fourierdlem14  43188  fourierdlem15  43189  fourierdlem17  43191  fourierdlem19  43193  fourierdlem30  43204  fourierdlem37  43211  fourierdlem40  43214  fourierdlem41  43215  fourierdlem42  43216  fourierdlem47  43220  fourierdlem48  43221  fourierdlem49  43222  fourierdlem50  43223  fourierdlem51  43224  fourierdlem54  43227  fourierdlem63  43236  fourierdlem64  43237  fourierdlem65  43238  fourierdlem68  43241  fourierdlem73  43246  fourierdlem74  43247  fourierdlem76  43249  fourierdlem77  43250  fourierdlem78  43251  fourierdlem79  43252  fourierdlem81  43254  fourierdlem82  43255  fourierdlem83  43256  fourierdlem92  43265  fourierdlem93  43266  fourierdlem102  43275  fourierdlem103  43276  fourierdlem104  43277  fourierdlem107  43280  fourierdlem111  43284  fourierdlem114  43287  sqwvfoura  43295  sqwvfourb  43296  fouriersw  43298  etransclem19  43320  etransclem23  43324  etransclem35  43336  etransclem41  43342  qndenserrnbllem  43361  iundjiun  43524  carageniuncllem2  43586  caratheodorylem1  43590  hoicvr  43612  ovnsubaddlem1  43634  hsphoidmvle2  43649  hoidmv1lelem1  43655  hoidmv1lelem2  43656  hoidmvlelem1  43659  hoidmvlelem2  43660  hoidmvlelem3  43661  hoiqssbllem1  43686  hoiqssbllem2  43687  volico2  43705  iinhoiicclem  43737  iunhoiioolem  43739  vonioolem2  43745  vonicclem2  43748  pimdecfgtioo  43777  pimincfltioo  43778  smflimlem4  43832  smfmullem1  43848  smflimsuplem4  43879  expnegico01  45377  eenglngeehlnmlem2  45602  inlinecirc02plem  45650