MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ltled Structured version   Visualization version   GIF version

Theorem ltled 10780
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
StepHypRef Expression
1 ltled.1 . 2 (𝜑𝐴 < 𝐵)
2 ltd.1 . . 3 (𝜑𝐴 ∈ ℝ)
3 ltd.2 . . 3 (𝜑𝐵 ∈ ℝ)
4 ltle 10721 . . 3 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵𝐴𝐵))
52, 3, 4syl2anc 586 . 2 (𝜑 → (𝐴 < 𝐵𝐴𝐵))
61, 5mpd 15 1 (𝜑𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107   class class class wbr 5057  cr 10528   < clt 10667  cle 10668
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7453  ax-resscn 10586  ax-pre-lttri 10603
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ne 3015  df-nel 3122  df-ral 3141  df-rex 3142  df-rab 3145  df-v 3495  df-sbc 3771  df-csb 3882  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4831  df-br 5058  df-opab 5120  df-mpt 5138  df-id 5453  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-er 8281  df-en 8502  df-dom 8503  df-sdom 8504  df-pnf 10669  df-mnf 10670  df-xr 10671  df-ltxr 10672  df-le 10673
This theorem is referenced by:  ltnsymd  10781  mulge0  11150  msqge0  11153  addgt0d  11207  lt2addd  11255  lt2msq1  11516  uzwo3  12335  fznatpl1  12953  flflp1  13169  modaddmodup  13294  expmulnbnd  13588  fzsdom2  13781  repswcshw  14166  isercolllem1  15013  caucvgrlem  15021  climcnds  15198  geomulcvg  15224  mertenslem1  15232  ruclem2  15577  ruclem12  15586  bitsfzo  15776  bitsmod  15777  lcmgcdlem  15942  isprm7  16044  4sqlem7  16272  vdwlem1  16309  met1stc  23123  cfilucfil  23161  nlmvscnlem2  23286  icccmplem2  23423  reconnlem2  23427  xrhmeo  23542  cnheibor  23551  nmoleub2lem3  23711  ipcnlem2  23839  minveclem3b  24023  ivthlem1  24044  ivthlem2  24045  ivth2  24048  ivthle  24049  ivthle2  24050  ovollb2lem  24081  ovolicc2lem4  24113  ovolicc2lem5  24114  ioombl1lem4  24154  uniioombllem4  24179  uniioombllem5  24180  opnmbllem  24194  ismbf3d  24247  mbfi1fseqlem6  24313  itg2gt0  24353  dveflem  24568  dvferm1lem  24573  dvferm2lem  24575  rollelem  24578  rolle  24579  cmvth  24580  mvth  24581  c1liplem1  24585  dvgt0lem1  24591  dvivthlem1  24597  lhop1lem  24602  lhop1  24603  dvcnvrelem1  24606  dvcnvrelem2  24607  dvcvx  24609  dgradd2  24850  aaliou3lem8  24926  aaliou3lem7  24930  ulmdvlem1  24980  itgulm  24988  radcnvlt1  24998  radcnvle  25000  abelthlem7  25018  efcvx  25029  coseq0negpitopi  25081  tangtx  25083  tanabsge  25084  tanord  25114  abslogimle  25149  divlogrlim  25210  logno1  25211  logcnlem3  25219  logcnlem4  25220  logtayl  25235  logccv  25238  cxple  25270  chordthmlem4  25405  asinsin  25462  atanlogaddlem  25483  atantan  25493  cxp2limlem  25545  logdifbnd  25563  emcllem4  25568  harmonicbnd4  25580  lgamucov  25607  ftalem1  25642  ftalem2  25643  ftalem3  25644  basellem5  25654  basellem8  25657  chpchtsum  25787  bposlem1  25852  lgseisenlem1  25943  lgsquadlem1  25948  lgsquadlem2  25949  lgsquadlem3  25950  2sqreulem1  26014  2sqreunnlem1  26017  chebbnd1lem2  26038  chebbnd1lem3  26039  chtppilimlem1  26041  chto1ub  26044  chpo1ubb  26049  vmadivsumb  26051  dchrisumlem3  26059  mulog2sumlem1  26102  vmalogdivsum2  26106  vmalogdivsum  26107  2vmadivsumlem  26108  selbergb  26117  selberg2b  26120  chpdifbndlem1  26121  selberg3lem2  26126  selberg3  26127  selberg4lem1  26128  selberg4  26129  pntrsumbnd  26134  selberg3r  26137  selberg4r  26138  selberg34r  26139  pntrlog2bndlem1  26145  pntrlog2bndlem2  26146  pntrlog2bndlem3  26147  pntrlog2bndlem4  26148  pntrlog2bndlem5  26149  pntrlog2bndlem6a  26150  pntrlog2bndlem6  26151  pntrlog2bnd  26152  pntpbnd1a  26153  pntpbnd1  26154  pntpbnd2  26155  pntibndlem2  26159  pntlemb  26165  pntlemq  26169  pntlemr  26170  pntlemj  26171  pntlemf  26173  pntlemp  26178  ostth2lem2  26202  axpaschlem  26718  axlowdimlem16  26735  smcnlem  28466  bcm1n  30510  wrdt2ind  30620  cycpmco2lem6  30766  cyc3conja  30792  smatrcl  31049  fiunelros  31421  dya2icoseg  31523  eulerpartlemgc  31608  dstfrvunirn  31720  ballotlemfc0  31738  ballotlemfcc  31739  ballotlemimin  31751  ballotlemsgt1  31756  ballotlemfrcn0  31775  sgnmul  31788  fdvposlt  31858  breprexp  31892  logdivsqrle  31909  hgt750leme  31917  tgoldbachgt  31922  lpadmax  31941  lpadright  31943  subfacval3  32424  erdszelem8  32433  cvmliftlem6  32525  cvmliftlem7  32526  cvmliftlem8  32527  cvmliftlem9  32528  cvmliftlem10  32529  sinccvglem  32903  dnibndlem9  33813  unbdqndv2lem2  33837  knoppndvlem14  33852  knoppndvlem18  33856  knoppndvlem19  33857  poimirlem7  34886  poimirlem15  34894  opnmbllem0  34915  itg2addnclem  34930  itg2addnclem3  34932  itg2addnc  34933  itg2gt0cn  34934  areacirclem1  34969  areacirc  34974  isbnd3  35049  cntotbnd  35061  rrnequiv  35100  nn0rppwr  39167  nn0expgcd  39169  rtprmirr  39179  fltnltalem  39259  irrapxlem3  39406  pellexlem2  39412  pellfundglb  39467  monotuz  39523  monotoddzzfi  39524  acongrep  39562  cvgdvgrat  40630  hashnzfz2  40638  hashnzfzclim  40639  binomcxplemnotnn0  40673  monoords  41548  xralrple2  41606  reclt0d  41642  reclt0  41647  uzublem  41688  iooiinicc  41802  iooiinioc  41816  limciccioolb  41886  limcicciooub  41902  lptre2pt  41905  limsupubuzlem  41977  limsup10exlem  42037  icccncfext  42154  cncfiooicclem1  42160  dvdivbd  42192  dvbdfbdioolem1  42197  dvbdfbdioolem2  42198  ioodvbdlimc1lem2  42201  ioodvbdlimc2lem  42203  dvnxpaek  42211  dvnmul  42212  volioc  42241  iblspltprt  42242  itgspltprt  42248  volico  42253  volioore  42260  voliooico  42262  voliccico  42269  stoweidlem1  42271  stoweidlem3  42273  stoweidlem7  42277  stoweidlem24  42294  stoweidlem26  42296  stoweidlem42  42312  wallispilem5  42339  stirlinglem1  42344  stirlinglem6  42349  stirlinglem7  42350  stirlinglem10  42353  stirlinglem12  42355  stirlinglem13  42356  stirlingr  42360  dirkertrigeqlem1  42368  fourierdlem10  42387  fourierdlem11  42388  fourierdlem12  42389  fourierdlem14  42391  fourierdlem15  42392  fourierdlem17  42394  fourierdlem19  42396  fourierdlem30  42407  fourierdlem37  42414  fourierdlem40  42417  fourierdlem41  42418  fourierdlem42  42419  fourierdlem47  42423  fourierdlem48  42424  fourierdlem49  42425  fourierdlem50  42426  fourierdlem51  42427  fourierdlem54  42430  fourierdlem63  42439  fourierdlem64  42440  fourierdlem65  42441  fourierdlem68  42444  fourierdlem73  42449  fourierdlem74  42450  fourierdlem76  42452  fourierdlem77  42453  fourierdlem78  42454  fourierdlem79  42455  fourierdlem81  42457  fourierdlem82  42458  fourierdlem83  42459  fourierdlem92  42468  fourierdlem93  42469  fourierdlem102  42478  fourierdlem103  42479  fourierdlem104  42480  fourierdlem107  42483  fourierdlem111  42487  fourierdlem114  42490  sqwvfoura  42498  sqwvfourb  42499  fouriersw  42501  etransclem19  42523  etransclem23  42527  etransclem35  42539  etransclem41  42545  qndenserrnbllem  42564  iundjiun  42727  carageniuncllem2  42789  caratheodorylem1  42793  hoicvr  42815  ovnsubaddlem1  42837  hsphoidmvle2  42852  hoidmv1lelem1  42858  hoidmv1lelem2  42859  hoidmvlelem1  42862  hoidmvlelem2  42863  hoidmvlelem3  42864  hoiqssbllem1  42889  hoiqssbllem2  42890  volico2  42908  iinhoiicclem  42940  iunhoiioolem  42942  vonioolem2  42948  vonicclem2  42951  pimdecfgtioo  42980  pimincfltioo  42981  smflimlem4  43035  smfmullem1  43051  smflimsuplem4  43082  expnegico01  44558  eenglngeehlnmlem2  44710  inlinecirc02plem  44758
  Copyright terms: Public domain W3C validator