Theorem ltled 11298

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

Syntax hints:   → wi 4   ∈ wcel 2109   class class class wbr 5102  ℝcr 11043   < clt 11184   ≤ cle 11185

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7691  ax-resscn 11101  ax-pre-lttri 11118

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-er 8648  df-en 8896  df-dom 8897  df-sdom 8898  df-pnf 11186  df-mnf 11187  df-xr 11188  df-ltxr 11189  df-le 11190

This theorem is referenced by:  ltnsymd  11299  mulge0  11672  msqge0  11675  addgt0d  11729  lt2addd  11777  lt2msq1  12043  uzwo3  12878  fznatpl1  13515  flflp1  13745  modaddmodup  13875  expmulnbnd  14176  fzsdom2  14369  repswcshw  14753  isercolllem1  15607  caucvgrlem  15615  climcnds  15793  geomulcvg  15818  mertenslem1  15826  ruclem2  16176  ruclem12  16185  bitsfzo  16381  bitsmod  16382  nn0rppwr  16507  nn0expgcd  16510  lcmgcdlem  16552  isprm7  16654  4sqlem7  16891  vdwlem1  16928  met1stc  24385  cfilucfil  24423  nlmvscnlem2  24549  icccmplem2  24688  reconnlem2  24692  xrhmeo  24820  cnheibor  24830  nmoleub2lem3  24991  ipcnlem2  25120  minveclem3b  25304  ivthlem1  25328  ivthlem2  25329  ivth2  25332  ivthle  25333  ivthle2  25334  ovollb2lem  25365  ovolicc2lem4  25397  ovolicc2lem5  25398  ioombl1lem4  25438  uniioombllem4  25463  uniioombllem5  25464  opnmbllem  25478  ismbf3d  25531  mbfi1fseqlem6  25597  itg2gt0  25637  dveflem  25859  dvferm1lem  25864  dvferm2lem  25866  rollelem  25869  rolle  25870  cmvth  25871  cmvthOLD  25872  mvth  25873  c1liplem1  25877  dvgt0lem1  25883  dvivthlem1  25889  lhop1lem  25894  lhop1  25895  dvcnvrelem1  25898  dvcnvrelem2  25899  dvcvx  25901  dgradd2  26150  aaliou3lem8  26229  aaliou3lem7  26233  ulmdvlem1  26285  itgulm  26293  radcnvlt1  26303  radcnvle  26305  abelthlem7  26324  efcvx  26335  coseq0negpitopi  26388  tangtx  26390  tanabsge  26391  tanord  26423  abslogimle  26458  divlogrlim  26520  logno1  26521  logcnlem3  26529  logcnlem4  26530  logtayl  26545  logccv  26548  cxple  26580  rtprmirr  26646  chordthmlem4  26721  asinsin  26778  atanlogaddlem  26799  atantan  26809  cxp2limlem  26862  logdifbnd  26880  emcllem4  26885  harmonicbnd4  26897  lgamucov  26924  ftalem1  26959  ftalem2  26960  ftalem3  26961  basellem5  26971  basellem8  26974  chpchtsum  27106  bposlem1  27171  lgseisenlem1  27262  lgsquadlem1  27267  lgsquadlem2  27268  lgsquadlem3  27269  2sqreulem1  27333  2sqreunnlem1  27336  chebbnd1lem2  27357  chebbnd1lem3  27358  chtppilimlem1  27360  chto1ub  27363  chpo1ubb  27368  vmadivsumb  27370  dchrisumlem3  27378  mulog2sumlem1  27421  vmalogdivsum2  27425  vmalogdivsum  27426  2vmadivsumlem  27427  selbergb  27436  selberg2b  27439  chpdifbndlem1  27440  selberg3lem2  27445  selberg3  27446  selberg4lem1  27447  selberg4  27448  pntrsumbnd  27453  selberg3r  27456  selberg4r  27457  selberg34r  27458  pntrlog2bndlem1  27464  pntrlog2bndlem2  27465  pntrlog2bndlem3  27466  pntrlog2bndlem4  27467  pntrlog2bndlem5  27468  pntrlog2bndlem6a  27469  pntrlog2bndlem6  27470  pntrlog2bnd  27471  pntpbnd1a  27472  pntpbnd1  27473  pntpbnd2  27474  pntibndlem2  27478  pntlemb  27484  pntlemq  27488  pntlemr  27489  pntlemj  27490  pntlemf  27492  pntlemp  27497  ostth2lem2  27521  axpaschlem  28843  axlowdimlem16  28860  smcnlem  30599  bcm1n  32691  sgnmul  32733  wrdt2ind  32848  chnub  32911  cycpmco2lem6  33061  cyc3conja  33087  smatrcl  33759  fiunelros  34137  dya2icoseg  34241  eulerpartlemgc  34326  dstfrvunirn  34439  ballotlemfc0  34457  ballotlemfcc  34458  ballotlemimin  34470  ballotlemsgt1  34475  ballotlemfrcn0  34494  fdvposlt  34563  breprexp  34597  logdivsqrle  34614  hgt750leme  34622  tgoldbachgt  34627  lpadmax  34646  lpadright  34648  subfacval3  35149  erdszelem8  35158  cvmliftlem6  35250  cvmliftlem7  35251  cvmliftlem8  35252  cvmliftlem9  35253  cvmliftlem10  35254  sinccvglem  35632  dnibndlem9  36447  unbdqndv2lem2  36471  knoppndvlem14  36486  knoppndvlem18  36490  knoppndvlem19  36491  poimirlem7  37594  poimirlem15  37602  opnmbllem0  37623  itg2addnclem  37638  itg2addnclem3  37640  itg2addnc  37641  itg2gt0cn  37642  areacirclem1  37675  areacirc  37680  isbnd3  37751  cntotbnd  37763  rrnequiv  37802  lcmineqlem11  42000  lcmineqlem22  42011  3lexlogpow5ineq2  42016  3lexlogpow5ineq5  42021  dvrelogpow2b  42029  aks4d1p1p2  42031  aks4d1p1p4  42032  aks4d1p1p6  42034  aks4d1p1p7  42035  aks4d1p1p5  42036  aks4d1p1  42037  aks4d1p2  42038  aks4d1p3  42039  aks4d1p5  42041  aks4d1p7d1  42043  aks4d1p7  42044  aks4d1p8  42048  hashscontpow1  42082  aks6d1c2lem4  42088  aks6d1c5lem2  42099  sticksstones6  42112  sticksstones12a  42118  sticksstones12  42119  aks6d1c7lem1  42141  unitscyglem2  42157  posqsqznn  42297  redvmptabs  42321  readvrec  42323  fltnltalem  42623  irrapxlem3  42785  pellexlem2  42791  pellfundglb  42846  monotuz  42903  monotoddzzfi  42904  acongrep  42942  cvgdvgrat  44275  hashnzfz2  44283  hashnzfzclim  44284  binomcxplemnotnn0  44318  monoords  45268  xralrple2  45323  reclt0d  45356  reclt0  45360  uzublem  45399  cvgcaule  45460  iooiinicc  45513  iooiinioc  45527  limciccioolb  45592  limcicciooub  45608  lptre2pt  45611  limsupubuzlem  45683  limsup10exlem  45743  icccncfext  45858  cncfiooicclem1  45864  dvdivbd  45894  dvbdfbdioolem1  45899  dvbdfbdioolem2  45900  ioodvbdlimc1lem2  45903  ioodvbdlimc2lem  45905  dvnxpaek  45913  dvnmul  45914  volioc  45943  iblspltprt  45944  itgspltprt  45950  volico  45954  volioore  45961  voliooico  45963  voliccico  45970  stoweidlem1  45972  stoweidlem3  45974  stoweidlem7  45978  stoweidlem24  45995  stoweidlem26  45997  stoweidlem42  46013  wallispilem5  46040  stirlinglem1  46045  stirlinglem6  46050  stirlinglem7  46051  stirlinglem10  46054  stirlinglem12  46056  stirlinglem13  46057  stirlingr  46061  dirkertrigeqlem1  46069  fourierdlem10  46088  fourierdlem11  46089  fourierdlem12  46090  fourierdlem14  46092  fourierdlem15  46093  fourierdlem17  46095  fourierdlem19  46097  fourierdlem30  46108  fourierdlem37  46115  fourierdlem40  46118  fourierdlem41  46119  fourierdlem42  46120  fourierdlem47  46124  fourierdlem48  46125  fourierdlem49  46126  fourierdlem50  46127  fourierdlem51  46128  fourierdlem54  46131  fourierdlem63  46140  fourierdlem64  46141  fourierdlem65  46142  fourierdlem68  46145  fourierdlem73  46150  fourierdlem74  46151  fourierdlem76  46153  fourierdlem77  46154  fourierdlem78  46155  fourierdlem79  46156  fourierdlem81  46158  fourierdlem82  46159  fourierdlem83  46160  fourierdlem92  46169  fourierdlem93  46170  fourierdlem102  46179  fourierdlem103  46180  fourierdlem104  46181  fourierdlem107  46184  fourierdlem111  46188  fourierdlem114  46191  sqwvfoura  46199  sqwvfourb  46200  fouriersw  46202  etransclem19  46224  etransclem23  46228  etransclem35  46240  etransclem41  46246  qndenserrnbllem  46265  iundjiun  46431  carageniuncllem2  46493  caratheodorylem1  46497  hoicvr  46519  ovnsubaddlem1  46541  hsphoidmvle2  46556  hoidmv1lelem1  46562  hoidmv1lelem2  46563  hoidmvlelem1  46566  hoidmvlelem2  46567  hoidmvlelem3  46568  hoiqssbllem1  46593  hoiqssbllem2  46594  volico2  46612  iinhoiicclem  46644  iunhoiioolem  46646  vonioolem2  46652  vonicclem2  46655  pimdecfgtioo  46688  pimincfltioo  46689  smflimlem4  46745  smfmullem1  46762  smflimsuplem4  46794  gpg3kgrtriexlem4  48050  gpg3kgrtriexlem6  48052  expnegico01  48480  eenglngeehlnmlem2  48700  inlinecirc02plem  48748