Theorem ltled 11368

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

Syntax hints:   → wi 4   ∈ wcel 2104   class class class wbr 5149  ℝcr 11113   < clt 11254   ≤ cle 11255

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7729  ax-resscn 11171  ax-pre-lttri 11188

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-er 8707  df-en 8944  df-dom 8945  df-sdom 8946  df-pnf 11256  df-mnf 11257  df-xr 11258  df-ltxr 11259  df-le 11260

This theorem is referenced by:  ltnsymd  11369  mulge0  11738  msqge0  11741  addgt0d  11795  lt2addd  11843  lt2msq1  12104  uzwo3  12933  fznatpl1  13561  flflp1  13778  modaddmodup  13905  expmulnbnd  14204  fzsdom2  14394  repswcshw  14768  isercolllem1  15617  caucvgrlem  15625  climcnds  15803  geomulcvg  15828  mertenslem1  15836  ruclem2  16181  ruclem12  16190  bitsfzo  16382  bitsmod  16383  lcmgcdlem  16549  isprm7  16651  4sqlem7  16883  vdwlem1  16920  met1stc  24252  cfilucfil  24290  nlmvscnlem2  24424  icccmplem2  24561  reconnlem2  24565  xrhmeo  24693  cnheibor  24703  nmoleub2lem3  24864  ipcnlem2  24994  minveclem3b  25178  ivthlem1  25202  ivthlem2  25203  ivth2  25206  ivthle  25207  ivthle2  25208  ovollb2lem  25239  ovolicc2lem4  25271  ovolicc2lem5  25272  ioombl1lem4  25312  uniioombllem4  25337  uniioombllem5  25338  opnmbllem  25352  ismbf3d  25405  mbfi1fseqlem6  25472  itg2gt0  25512  dveflem  25730  dvferm1lem  25735  dvferm2lem  25737  rollelem  25740  rolle  25741  cmvth  25742  mvth  25743  c1liplem1  25747  dvgt0lem1  25753  dvivthlem1  25759  lhop1lem  25764  lhop1  25765  dvcnvrelem1  25768  dvcnvrelem2  25769  dvcvx  25771  dgradd2  26016  aaliou3lem8  26092  aaliou3lem7  26096  ulmdvlem1  26146  itgulm  26154  radcnvlt1  26164  radcnvle  26166  abelthlem7  26184  efcvx  26195  coseq0negpitopi  26247  tangtx  26249  tanabsge  26250  tanord  26281  abslogimle  26316  divlogrlim  26377  logno1  26378  logcnlem3  26386  logcnlem4  26387  logtayl  26402  logccv  26405  cxple  26437  chordthmlem4  26574  asinsin  26631  atanlogaddlem  26652  atantan  26662  cxp2limlem  26714  logdifbnd  26732  emcllem4  26737  harmonicbnd4  26749  lgamucov  26776  ftalem1  26811  ftalem2  26812  ftalem3  26813  basellem5  26823  basellem8  26826  chpchtsum  26956  bposlem1  27021  lgseisenlem1  27112  lgsquadlem1  27117  lgsquadlem2  27118  lgsquadlem3  27119  2sqreulem1  27183  2sqreunnlem1  27186  chebbnd1lem2  27207  chebbnd1lem3  27208  chtppilimlem1  27210  chto1ub  27213  chpo1ubb  27218  vmadivsumb  27220  dchrisumlem3  27228  mulog2sumlem1  27271  vmalogdivsum2  27275  vmalogdivsum  27276  2vmadivsumlem  27277  selbergb  27286  selberg2b  27289  chpdifbndlem1  27290  selberg3lem2  27295  selberg3  27296  selberg4lem1  27297  selberg4  27298  pntrsumbnd  27303  selberg3r  27306  selberg4r  27307  selberg34r  27308  pntrlog2bndlem1  27314  pntrlog2bndlem2  27315  pntrlog2bndlem3  27316  pntrlog2bndlem4  27317  pntrlog2bndlem5  27318  pntrlog2bndlem6a  27319  pntrlog2bndlem6  27320  pntrlog2bnd  27321  pntpbnd1a  27322  pntpbnd1  27323  pntpbnd2  27324  pntibndlem2  27328  pntlemb  27334  pntlemq  27338  pntlemr  27339  pntlemj  27340  pntlemf  27342  pntlemp  27347  ostth2lem2  27371  axpaschlem  28463  axlowdimlem16  28480  smcnlem  30215  bcm1n  32271  wrdt2ind  32382  cycpmco2lem6  32558  cyc3conja  32584  smatrcl  33072  fiunelros  33468  dya2icoseg  33572  eulerpartlemgc  33657  dstfrvunirn  33769  ballotlemfc0  33787  ballotlemfcc  33788  ballotlemimin  33800  ballotlemsgt1  33805  ballotlemfrcn0  33824  sgnmul  33837  fdvposlt  33907  breprexp  33941  logdivsqrle  33958  hgt750leme  33966  tgoldbachgt  33971  lpadmax  33990  lpadright  33992  subfacval3  34476  erdszelem8  34485  cvmliftlem6  34577  cvmliftlem7  34578  cvmliftlem8  34579  cvmliftlem9  34580  cvmliftlem10  34581  sinccvglem  34953  gg-cmvth  35469  dnibndlem9  35667  unbdqndv2lem2  35691  knoppndvlem14  35706  knoppndvlem18  35710  knoppndvlem19  35711  poimirlem7  36800  poimirlem15  36808  opnmbllem0  36829  itg2addnclem  36844  itg2addnclem3  36846  itg2addnc  36847  itg2gt0cn  36848  areacirclem1  36881  areacirc  36886  isbnd3  36957  cntotbnd  36969  rrnequiv  37008  lcmineqlem11  41212  lcmineqlem22  41223  3lexlogpow5ineq2  41228  3lexlogpow5ineq5  41233  dvrelogpow2b  41241  aks4d1p1p2  41243  aks4d1p1p4  41244  aks4d1p1p6  41246  aks4d1p1p7  41247  aks4d1p1p5  41248  aks4d1p1  41249  aks4d1p2  41250  aks4d1p3  41251  aks4d1p5  41253  aks4d1p7d1  41255  aks4d1p7  41256  aks4d1p8  41260  sticksstones6  41275  sticksstones12a  41281  sticksstones12  41282  metakunt7  41299  metakunt29  41321  metakunt30  41322  nn0rppwr  41528  nn0expgcd  41530  posqsqznn  41538  rtprmirr  41541  fltnltalem  41708  irrapxlem3  41866  pellexlem2  41872  pellfundglb  41927  monotuz  41984  monotoddzzfi  41985  acongrep  42023  cvgdvgrat  43376  hashnzfz2  43384  hashnzfzclim  43385  binomcxplemnotnn0  43419  monoords  44307  xralrple2  44364  reclt0d  44397  reclt0  44401  uzublem  44440  cvgcaule  44502  iooiinicc  44555  iooiinioc  44569  limciccioolb  44637  limcicciooub  44653  lptre2pt  44656  limsupubuzlem  44728  limsup10exlem  44788  icccncfext  44903  cncfiooicclem1  44909  dvdivbd  44939  dvbdfbdioolem1  44944  dvbdfbdioolem2  44945  ioodvbdlimc1lem2  44948  ioodvbdlimc2lem  44950  dvnxpaek  44958  dvnmul  44959  volioc  44988  iblspltprt  44989  itgspltprt  44995  volico  44999  volioore  45006  voliooico  45008  voliccico  45015  stoweidlem1  45017  stoweidlem3  45019  stoweidlem7  45023  stoweidlem24  45040  stoweidlem26  45042  stoweidlem42  45058  wallispilem5  45085  stirlinglem1  45090  stirlinglem6  45095  stirlinglem7  45096  stirlinglem10  45099  stirlinglem12  45101  stirlinglem13  45102  stirlingr  45106  dirkertrigeqlem1  45114  fourierdlem10  45133  fourierdlem11  45134  fourierdlem12  45135  fourierdlem14  45137  fourierdlem15  45138  fourierdlem17  45140  fourierdlem19  45142  fourierdlem30  45153  fourierdlem37  45160  fourierdlem40  45163  fourierdlem41  45164  fourierdlem42  45165  fourierdlem47  45169  fourierdlem48  45170  fourierdlem49  45171  fourierdlem50  45172  fourierdlem51  45173  fourierdlem54  45176  fourierdlem63  45185  fourierdlem64  45186  fourierdlem65  45187  fourierdlem68  45190  fourierdlem73  45195  fourierdlem74  45196  fourierdlem76  45198  fourierdlem77  45199  fourierdlem78  45200  fourierdlem79  45201  fourierdlem81  45203  fourierdlem82  45204  fourierdlem83  45205  fourierdlem92  45214  fourierdlem93  45215  fourierdlem102  45224  fourierdlem103  45225  fourierdlem104  45226  fourierdlem107  45229  fourierdlem111  45233  fourierdlem114  45236  sqwvfoura  45244  sqwvfourb  45245  fouriersw  45247  etransclem19  45269  etransclem23  45273  etransclem35  45285  etransclem41  45291  qndenserrnbllem  45310  iundjiun  45476  carageniuncllem2  45538  caratheodorylem1  45542  hoicvr  45564  ovnsubaddlem1  45586  hsphoidmvle2  45601  hoidmv1lelem1  45607  hoidmv1lelem2  45608  hoidmvlelem1  45611  hoidmvlelem2  45612  hoidmvlelem3  45613  hoiqssbllem1  45638  hoiqssbllem2  45639  volico2  45657  iinhoiicclem  45689  iunhoiioolem  45691  vonioolem2  45697  vonicclem2  45700  pimdecfgtioo  45733  pimincfltioo  45734  smflimlem4  45790  smfmullem1  45807  smflimsuplem4  45839  expnegico01  47288  eenglngeehlnmlem2  47513  inlinecirc02plem  47561