Theorem ltled 11369

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146   class class class wbr 5111  ℝcr 11110   < clt 11254   ≤ cle 11255

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 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7738  ax-resscn 11168  ax-pre-lttri 11185

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 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3067  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-er 8696  df-en 8946  df-dom 8947  df-sdom 8948  df-pnf 11256  df-mnf 11257  df-xr 11258  df-ltxr 11259  df-le 11260

This theorem is used by:  ltnsymd  11370  mulge0  11743  msqge0  11746  addgt0d  11800  lt2addd  11848  lt2msq1  12110  uzwo3  12979  fznatpl1  13619  flflp1  13854  modaddmodup  13984  expmulnbnd  14285  fzsdom2  14479  repswcshw  14869  sgnmul  15164  isercolllem1  15736  caucvgrlem  15744  climcnds  15924  geomulcvg  15949  mertenslem1  15957  ruclem2  16306  ruclem12  16315  bitsfzo  16511  bitsmod  16512  nn0rppwr  16637  nn0expgcd  16640  lcmgcdlem  16682  isprm7  16785  4sqlem7  17022  vdwlem1  17059  chnub  18696  met1stc  24709  cfilucfil  24747  nlmvscnlem2  24873  icccmplem2  25012  reconnlem2  25016  xrhmeo  25136  cnheibor  25145  nmoleub2lem3  25305  ipcnlem2  25434  minveclem3b  25618  ivthlem1  25641  ivthlem2  25642  ivth2  25645  ivthle  25646  ivthle2  25647  ovollb2lem  25678  ovolicc2lem4  25710  ovolicc2lem5  25711  ioombl1lem4  25751  uniioombllem4  25776  uniioombllem5  25777  opnmbllem  25791  ismbf3d  25844  mbfi1fseqlem6  25910  itg2gt0  25950  dveflem  26169  dvferm1lem  26174  dvferm2lem  26176  rollelem  26179  rolle  26180  cmvth  26181  mvth  26182  c1liplem1  26186  dvgt0lem1  26192  dvivthlem1  26198  lhop1lem  26203  lhop1  26204  dvcnvrelem1  26207  dvcnvrelem2  26208  dvcvx  26210  dgradd2  26456  aaliou3lem8  26539  aaliou3lem7  26543  ulmdvlem1  26594  itgulm  26602  radcnvlt1  26612  radcnvle  26614  abelthlem7  26632  efcvx  26643  coseq0negpitopi  26699  tangtx  26701  tanabsge  26702  tanord  26734  abslogimle  26769  divlogrlim  26831  logno1  26832  logcnlem3  26840  logcnlem4  26841  logtayl  26856  logccv  26859  cxple  26891  rtprmirr  26956  chordthmlem4  27031  asinsin  27088  atanlogaddlem  27109  atantan  27119  cxp2limlem  27171  logdifbnd  27189  emcllem4  27194  harmonicbnd4  27206  lgamucov  27233  ftalem1  27268  ftalem2  27269  ftalem3  27270  basellem5  27280  basellem8  27283  chpchtsum  27414  bposlem1  27479  lgseisenlem1  27570  lgsquadlem1  27575  lgsquadlem2  27576  lgsquadlem3  27577  2sqreulem1  27641  2sqreunnlem1  27644  chebbnd1lem2  27665  chebbnd1lem3  27666  chtppilimlem1  27668  chto1ub  27671  chpo1ubb  27676  vmadivsumb  27678  dchrisumlem3  27686  mulog2sumlem1  27729  vmalogdivsum2  27733  vmalogdivsum  27734  2vmadivsumlem  27735  selbergb  27744  selberg2b  27747  chpdifbndlem1  27748  selberg3lem2  27753  selberg3  27754  selberg4lem1  27755  selberg4  27756  pntrsumbnd  27761  selberg3r  27764  selberg4r  27765  selberg34r  27766  pntrlog2bndlem1  27772  pntrlog2bndlem2  27773  pntrlog2bndlem3  27774  pntrlog2bndlem4  27775  pntrlog2bndlem5  27776  pntrlog2bndlem6a  27777  pntrlog2bndlem6  27778  pntrlog2bnd  27779  pntpbnd1a  27780  pntpbnd1  27781  pntpbnd2  27782  pntibndlem2  27786  pntlemb  27792  pntlemq  27796  pntlemr  27797  pntlemj  27798  pntlemf  27800  pntlemp  27805  ostth2lem2  27829  axpaschlem  29321  axlowdimlem16  29338  smcnlem  31096  bcm1n  33186  wrdt2ind  33315  cycpmco2lem6  33491  cyc3conja  33517  smatrcl  34226  fiunelros  34605  dya2icoseg  34708  eulerpartlemgc  34793  dstfrvunirn  34906  ballotlemfc0  34924  ballotlemfcc  34925  ballotlemimin  34937  ballotlemsgt1  34942  ballotlemfrcn0  34961  fdvposlt  35027  breprexp  35061  logdivsqrle  35078  hgt750leme  35086  tgoldbachgt  35091  lpadmax  35113  lpadright  35115  subfacval3  35694  erdszelem8  35703  cvmliftlem6  35795  cvmliftlem7  35796  cvmliftlem8  35797  cvmliftlem9  35798  cvmliftlem10  35799  sinccvglem  36177  dnibndlem9  37108  unbdqndv2lem2  37132  knoppndvlem14  37147  knoppndvlem18  37151  knoppndvlem19  37152  poimirlem7  38311  poimirlem15  38319  opnmbllem0  38340  itg2addnclem  38355  itg2addnclem3  38357  itg2addnc  38358  itg2gt0cn  38359  areacirclem1  38392  areacirc  38397  isbnd3  38468  cntotbnd  38480  rrnequiv  38519  lcmineqlem11  42839  lcmineqlem22  42850  3lexlogpow5ineq2  42855  3lexlogpow5ineq5  42860  dvrelogpow2b  42868  aks4d1p1p2  42870  aks4d1p1p4  42871  aks4d1p1p6  42873  aks4d1p1p7  42874  aks4d1p1p5  42875  aks4d1p1  42876  aks4d1p2  42877  aks4d1p3  42878  aks4d1p5  42880  aks4d1p7d1  42882  aks4d1p7  42883  aks4d1p8  42887  hashscontpow1  42921  aks6d1c2lem4  42927  aks6d1c5lem2  42938  sticksstones6  42951  sticksstones12a  42957  sticksstones12  42958  aks6d1c7lem1  42980  unitscyglem2  42996  posqsqznn  43130  redvmptabs  43154  readvrec  43156  fltnltalem  43427  irrapxlem3  43584  pellexlem2  43590  pellfundglb  43645  monotuz  43701  monotoddzzfi  43702  acongrep  43740  cvgdvgrat  45056  hashnzfz2  45064  hashnzfzclim  45065  binomcxplemnotnn0  45099  monoords  46049  xralrple2  46103  reclt0d  46135  reclt0  46139  uzublem  46177  cvgcaule  46238  iooiinicc  46291  iooiinioc  46305  limciccioolb  46370  limcicciooub  46384  lptre2pt  46387  limsupubuzlem  46459  limsup10exlem  46519  icccncfext  46634  cncfiooicclem1  46640  dvdivbd  46670  dvbdfbdioolem1  46675  dvbdfbdioolem2  46676  ioodvbdlimc1lem2  46679  ioodvbdlimc2lem  46681  dvnxpaek  46689  dvnmul  46690  volioc  46719  iblspltprt  46720  itgspltprt  46726  volico  46730  volioore  46737  voliooico  46739  voliccico  46746  stoweidlem1  46748  stoweidlem3  46750  stoweidlem7  46754  stoweidlem24  46771  stoweidlem26  46773  stoweidlem42  46789  wallispilem5  46816  stirlinglem1  46821  stirlinglem6  46826  stirlinglem7  46827  stirlinglem10  46830  stirlinglem12  46832  stirlinglem13  46833  stirlingr  46837  dirkertrigeqlem1  46845  fourierdlem10  46864  fourierdlem11  46865  fourierdlem12  46866  fourierdlem14  46868  fourierdlem15  46869  fourierdlem17  46871  fourierdlem19  46873  fourierdlem30  46884  fourierdlem37  46891  fourierdlem40  46894  fourierdlem41  46895  fourierdlem42  46896  fourierdlem47  46900  fourierdlem48  46901  fourierdlem49  46902  fourierdlem50  46903  fourierdlem51  46904  fourierdlem54  46907  fourierdlem63  46916  fourierdlem64  46917  fourierdlem65  46918  fourierdlem68  46921  fourierdlem73  46926  fourierdlem74  46927  fourierdlem76  46929  fourierdlem77  46930  fourierdlem78  46931  fourierdlem79  46932  fourierdlem81  46934  fourierdlem82  46935  fourierdlem83  46936  fourierdlem92  46945  fourierdlem93  46946  fourierdlem102  46955  fourierdlem103  46956  fourierdlem104  46957  fourierdlem107  46960  fourierdlem111  46964  fourierdlem114  46967  sqwvfoura  46975  sqwvfourb  46976  fouriersw  46978  etransclem19  47000  etransclem23  47004  etransclem35  47016  etransclem41  47022  qndenserrnbllem  47041  iundjiun  47207  carageniuncllem2  47269  caratheodorylem1  47273  hoicvr  47295  ovnsubaddlem1  47317  hsphoidmvle2  47332  hoidmv1lelem1  47338  hoidmv1lelem2  47339  hoidmvlelem1  47342  hoidmvlelem2  47343  hoidmvlelem3  47344  hoiqssbllem1  47369  hoiqssbllem2  47370  volico2  47388  iinhoiicclem  47420  iunhoiioolem  47422  vonioolem2  47428  vonicclem2  47431  pimdecfgtioo  47464  pimincfltioo  47465  smflimlem4  47521  smfmullem1  47538  smflimsuplem4  47570  gpg3kgrtriexlem4  48884  gpg3kgrtriexlem6  48886  expnegico01  49331  eenglngeehlnmlem2  49551  inlinecirc02plem  49599