Theorem ltled 10504

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

Syntax hints:   → wi 4   ∈ wcel 2166   class class class wbr 4873  ℝcr 10251   < clt 10391   ≤ cle 10392

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-8 2168  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2803  ax-sep 5005  ax-nul 5013  ax-pow 5065  ax-pr 5127  ax-un 7209  ax-resscn 10309  ax-pre-lttri 10326

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ne 3000  df-nel 3103  df-ral 3122  df-rex 3123  df-rab 3126  df-v 3416  df-sbc 3663  df-csb 3758  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-nul 4145  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-op 4404  df-uni 4659  df-br 4874  df-opab 4936  df-mpt 4953  df-id 5250  df-xp 5348  df-rel 5349  df-cnv 5350  df-co 5351  df-dm 5352  df-rn 5353  df-res 5354  df-ima 5355  df-iota 6086  df-fun 6125  df-fn 6126  df-f 6127  df-f1 6128  df-fo 6129  df-f1o 6130  df-fv 6131  df-er 8009  df-en 8223  df-dom 8224  df-sdom 8225  df-pnf 10393  df-mnf 10394  df-xr 10395  df-ltxr 10396  df-le 10397

This theorem is referenced by:  ltnsymd  10505  mulge0  10870  msqge0  10873  addgt0d  10927  lt2addd  10975  lt2msq1  11237  uzwo3  12066  fznatpl1  12688  flflp1  12903  modaddmodup  13028  expmulnbnd  13290  fzsdom2  13504  repswcshw  13933  isercolllem1  14772  caucvgrlem  14780  climcnds  14957  geomulcvg  14981  mertenslem1  14989  ruclem2  15335  ruclem12  15344  bitsfzo  15530  bitsmod  15531  lcmgcdlem  15692  isprm7  15791  4sqlem7  16019  vdwlem1  16056  met1stc  22696  cfilucfil  22734  nlmvscnlem2  22859  icccmplem2  22996  reconnlem2  23000  xrhmeo  23115  cnheibor  23124  nmoleub2lem3  23284  ipcnlem2  23412  minveclem3b  23596  ivthlem1  23617  ivthlem2  23618  ivth2  23621  ivthle  23622  ivthle2  23623  ovollb2lem  23654  ovolicc2lem4  23686  ovolicc2lem5  23687  ioombl1lem4  23727  uniioombllem4  23752  uniioombllem5  23753  opnmbllem  23767  ismbf3d  23820  mbfi1fseqlem6  23886  itg2gt0  23926  dveflem  24141  dvferm1lem  24146  dvferm2lem  24148  rollelem  24151  rolle  24152  cmvth  24153  mvth  24154  c1liplem1  24158  dvgt0lem1  24164  dvivthlem1  24170  lhop1lem  24175  lhop1  24176  dvcnvrelem1  24179  dvcnvrelem2  24180  dvcvx  24182  dgradd2  24423  aaliou3lem8  24499  aaliou3lem7  24503  ulmdvlem1  24553  itgulm  24561  radcnvlt1  24571  radcnvle  24573  abelthlem7  24591  efcvx  24602  coseq0negpitopi  24655  tangtx  24657  tanabsge  24658  tanord  24684  abslogimle  24719  divlogrlim  24780  logno1  24781  logcnlem3  24789  logcnlem4  24790  logtayl  24805  logccv  24808  cxple  24840  chordthmlem4  24975  asinsin  25032  atanlogaddlem  25053  atantan  25063  cxp2limlem  25115  logdifbnd  25133  emcllem4  25138  harmonicbnd4  25150  lgamucov  25177  ftalem1  25212  ftalem2  25213  ftalem3  25214  basellem5  25224  basellem8  25227  chpchtsum  25357  bposlem1  25422  lgseisenlem1  25513  lgsquadlem1  25518  lgsquadlem2  25519  lgsquadlem3  25520  chebbnd1lem2  25572  chebbnd1lem3  25573  chtppilimlem1  25575  chto1ub  25578  chpo1ubb  25583  vmadivsumb  25585  dchrisumlem3  25593  mulog2sumlem1  25636  vmalogdivsum2  25640  vmalogdivsum  25641  2vmadivsumlem  25642  selbergb  25651  selberg2b  25654  chpdifbndlem1  25655  selberg3lem2  25660  selberg3  25661  selberg4lem1  25662  selberg4  25663  pntrsumbnd  25668  selberg3r  25671  selberg4r  25672  selberg34r  25673  pntrlog2bndlem1  25679  pntrlog2bndlem2  25680  pntrlog2bndlem3  25681  pntrlog2bndlem4  25682  pntrlog2bndlem5  25683  pntrlog2bndlem6a  25684  pntrlog2bndlem6  25685  pntrlog2bnd  25686  pntpbnd1a  25687  pntpbnd1  25688  pntpbnd2  25689  pntibndlem2  25693  pntlemb  25699  pntlemq  25703  pntlemr  25704  pntlemj  25705  pntlemf  25707  pntlemp  25712  ostth2lem2  25736  axpaschlem  26239  axlowdimlem16  26256  smcnlem  28107  bcm1n  30101  smatrcl  30407  fiunelros  30782  dya2icoseg  30884  eulerpartlemgc  30969  dstfrvunirn  31082  ballotlemfc0  31100  ballotlemfcc  31101  ballotlemimin  31113  ballotlemsgt1  31118  ballotlemfrcn0  31137  sgnmul  31150  fdvposlt  31226  breprexp  31260  logdivsqrle  31277  hgt750leme  31285  tgoldbachgt  31290  subfacval3  31717  erdszelem8  31726  cvmliftlem6  31818  cvmliftlem7  31819  cvmliftlem8  31820  cvmliftlem9  31821  cvmliftlem10  31822  sinccvglem  32110  dnibndlem9  33009  unbdqndv2lem2  33033  knoppndvlem14  33048  knoppndvlem18  33052  knoppndvlem19  33053  poimirlem7  33960  poimirlem15  33968  opnmbllem0  33989  itg2addnclem  34004  itg2addnclem3  34006  itg2addnc  34007  itg2gt0cn  34008  areacirclem1  34043  areacirc  34048  isbnd3  34125  cntotbnd  34137  rrnequiv  34176  irrapxlem3  38232  pellexlem2  38238  pellfundglb  38293  monotuz  38349  monotoddzzfi  38350  acongrep  38390  cvgdvgrat  39352  hashnzfz2  39360  hashnzfzclim  39361  binomcxplemnotnn0  39395  monoords  40309  xralrple2  40367  reclt0d  40404  reclt0  40409  uzublem  40452  iooiinicc  40564  iooiinioc  40578  limciccioolb  40648  limcicciooub  40664  lptre2pt  40667  limsupubuzlem  40739  limsup10exlem  40799  icccncfext  40895  cncfiooicclem1  40901  dvdivbd  40933  dvbdfbdioolem1  40938  dvbdfbdioolem2  40939  ioodvbdlimc1lem2  40942  ioodvbdlimc2lem  40944  dvnxpaek  40952  dvnmul  40953  volioc  40982  iblspltprt  40983  itgspltprt  40989  volico  40994  volioore  41001  voliooico  41003  voliccico  41010  stoweidlem1  41012  stoweidlem3  41014  stoweidlem7  41018  stoweidlem24  41035  stoweidlem26  41037  stoweidlem42  41053  wallispilem5  41080  stirlinglem1  41085  stirlinglem6  41090  stirlinglem7  41091  stirlinglem10  41094  stirlinglem12  41096  stirlinglem13  41097  stirlingr  41101  dirkertrigeqlem1  41109  fourierdlem10  41128  fourierdlem11  41129  fourierdlem12  41130  fourierdlem14  41132  fourierdlem15  41133  fourierdlem17  41135  fourierdlem19  41137  fourierdlem30  41148  fourierdlem37  41155  fourierdlem40  41158  fourierdlem41  41159  fourierdlem42  41160  fourierdlem47  41164  fourierdlem48  41165  fourierdlem49  41166  fourierdlem50  41167  fourierdlem51  41168  fourierdlem54  41171  fourierdlem63  41180  fourierdlem64  41181  fourierdlem65  41182  fourierdlem68  41185  fourierdlem73  41190  fourierdlem74  41191  fourierdlem76  41193  fourierdlem77  41194  fourierdlem78  41195  fourierdlem79  41196  fourierdlem81  41198  fourierdlem82  41199  fourierdlem83  41200  fourierdlem92  41209  fourierdlem93  41210  fourierdlem102  41219  fourierdlem103  41220  fourierdlem104  41221  fourierdlem107  41224  fourierdlem111  41228  fourierdlem114  41231  sqwvfoura  41239  sqwvfourb  41240  fouriersw  41242  etransclem19  41264  etransclem23  41268  etransclem35  41280  etransclem41  41286  qndenserrnbllem  41305  iundjiun  41468  carageniuncllem2  41530  caratheodorylem1  41534  hoicvr  41556  ovnsubaddlem1  41578  hsphoidmvle2  41593  hoidmv1lelem1  41599  hoidmv1lelem2  41600  hoidmvlelem1  41603  hoidmvlelem2  41604  hoidmvlelem3  41605  hoiqssbllem1  41630  hoiqssbllem2  41631  volico2  41649  iinhoiicclem  41681  iunhoiioolem  41683  vonioolem2  41689  vonicclem2  41692  pimdecfgtioo  41721  pimincfltioo  41722  smflimlem4  41776  smfmullem1  41792  smflimsuplem4  41823  expnegico01  43155  eenglngeehlnmlem2  43289