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

Theorem ltled 10776
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 10717 . . 3 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵𝐴𝐵))
52, 3, 4syl2anc 584 . 2 (𝜑 → (𝐴 < 𝐵𝐴𝐵))
61, 5mpd 15 1 (𝜑𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2105   class class class wbr 5057  cr 10524   < clt 10663  cle 10664
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450  ax-resscn 10582  ax-pre-lttri 10599
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-nel 3121  df-ral 3140  df-rex 3141  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-op 4564  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 8278  df-en 8498  df-dom 8499  df-sdom 8500  df-pnf 10665  df-mnf 10666  df-xr 10667  df-ltxr 10668  df-le 10669
This theorem is referenced by:  ltnsymd  10777  mulge0  11146  msqge0  11149  addgt0d  11203  lt2addd  11251  lt2msq1  11512  uzwo3  12331  fznatpl1  12949  flflp1  13165  modaddmodup  13290  expmulnbnd  13584  fzsdom2  13777  repswcshw  14162  isercolllem1  15009  caucvgrlem  15017  climcnds  15194  geomulcvg  15220  mertenslem1  15228  ruclem2  15573  ruclem12  15582  bitsfzo  15772  bitsmod  15773  lcmgcdlem  15938  isprm7  16040  4sqlem7  16268  vdwlem1  16305  met1stc  23058  cfilucfil  23096  nlmvscnlem2  23221  icccmplem2  23358  reconnlem2  23362  xrhmeo  23477  cnheibor  23486  nmoleub2lem3  23646  ipcnlem2  23774  minveclem3b  23958  ivthlem1  23979  ivthlem2  23980  ivth2  23983  ivthle  23984  ivthle2  23985  ovollb2lem  24016  ovolicc2lem4  24048  ovolicc2lem5  24049  ioombl1lem4  24089  uniioombllem4  24114  uniioombllem5  24115  opnmbllem  24129  ismbf3d  24182  mbfi1fseqlem6  24248  itg2gt0  24288  dveflem  24503  dvferm1lem  24508  dvferm2lem  24510  rollelem  24513  rolle  24514  cmvth  24515  mvth  24516  c1liplem1  24520  dvgt0lem1  24526  dvivthlem1  24532  lhop1lem  24537  lhop1  24538  dvcnvrelem1  24541  dvcnvrelem2  24542  dvcvx  24544  dgradd2  24785  aaliou3lem8  24861  aaliou3lem7  24865  ulmdvlem1  24915  itgulm  24923  radcnvlt1  24933  radcnvle  24935  abelthlem7  24953  efcvx  24964  coseq0negpitopi  25016  tangtx  25018  tanabsge  25019  tanord  25049  abslogimle  25084  divlogrlim  25145  logno1  25146  logcnlem3  25154  logcnlem4  25155  logtayl  25170  logccv  25173  cxple  25205  chordthmlem4  25340  asinsin  25397  atanlogaddlem  25418  atantan  25428  cxp2limlem  25480  logdifbnd  25498  emcllem4  25503  harmonicbnd4  25515  lgamucov  25542  ftalem1  25577  ftalem2  25578  ftalem3  25579  basellem5  25589  basellem8  25592  chpchtsum  25722  bposlem1  25787  lgseisenlem1  25878  lgsquadlem1  25883  lgsquadlem2  25884  lgsquadlem3  25885  2sqreulem1  25949  2sqreunnlem1  25952  chebbnd1lem2  25973  chebbnd1lem3  25974  chtppilimlem1  25976  chto1ub  25979  chpo1ubb  25984  vmadivsumb  25986  dchrisumlem3  25994  mulog2sumlem1  26037  vmalogdivsum2  26041  vmalogdivsum  26042  2vmadivsumlem  26043  selbergb  26052  selberg2b  26055  chpdifbndlem1  26056  selberg3lem2  26061  selberg3  26062  selberg4lem1  26063  selberg4  26064  pntrsumbnd  26069  selberg3r  26072  selberg4r  26073  selberg34r  26074  pntrlog2bndlem1  26080  pntrlog2bndlem2  26081  pntrlog2bndlem3  26082  pntrlog2bndlem4  26083  pntrlog2bndlem5  26084  pntrlog2bndlem6a  26085  pntrlog2bndlem6  26086  pntrlog2bnd  26087  pntpbnd1a  26088  pntpbnd1  26089  pntpbnd2  26090  pntibndlem2  26094  pntlemb  26100  pntlemq  26104  pntlemr  26105  pntlemj  26106  pntlemf  26108  pntlemp  26113  ostth2lem2  26137  axpaschlem  26653  axlowdimlem16  26670  smcnlem  28401  bcm1n  30444  wrdt2ind  30554  cycpmco2lem6  30700  cyc3conja  30726  smatrcl  30960  fiunelros  31332  dya2icoseg  31434  eulerpartlemgc  31519  dstfrvunirn  31631  ballotlemfc0  31649  ballotlemfcc  31650  ballotlemimin  31662  ballotlemsgt1  31667  ballotlemfrcn0  31686  sgnmul  31699  fdvposlt  31769  breprexp  31803  logdivsqrle  31820  hgt750leme  31828  tgoldbachgt  31833  lpadmax  31852  lpadright  31854  subfacval3  32333  erdszelem8  32342  cvmliftlem6  32434  cvmliftlem7  32435  cvmliftlem8  32436  cvmliftlem9  32437  cvmliftlem10  32438  sinccvglem  32812  dnibndlem9  33722  unbdqndv2lem2  33746  knoppndvlem14  33761  knoppndvlem18  33765  knoppndvlem19  33766  poimirlem7  34780  poimirlem15  34788  opnmbllem0  34809  itg2addnclem  34824  itg2addnclem3  34826  itg2addnc  34827  itg2gt0cn  34828  areacirclem1  34863  areacirc  34868  isbnd3  34943  cntotbnd  34955  rrnequiv  34994  nn0rppwr  39060  nn0expgcd  39062  rtprmirr  39072  fltnltalem  39152  irrapxlem3  39299  pellexlem2  39305  pellfundglb  39360  monotuz  39416  monotoddzzfi  39417  acongrep  39455  cvgdvgrat  40522  hashnzfz2  40530  hashnzfzclim  40531  binomcxplemnotnn0  40565  monoords  41440  xralrple2  41498  reclt0d  41534  reclt0  41539  uzublem  41580  iooiinicc  41694  iooiinioc  41708  limciccioolb  41778  limcicciooub  41794  lptre2pt  41797  limsupubuzlem  41869  limsup10exlem  41929  icccncfext  42046  cncfiooicclem1  42052  dvdivbd  42084  dvbdfbdioolem1  42089  dvbdfbdioolem2  42090  ioodvbdlimc1lem2  42093  ioodvbdlimc2lem  42095  dvnxpaek  42103  dvnmul  42104  volioc  42133  iblspltprt  42134  itgspltprt  42140  volico  42145  volioore  42152  voliooico  42154  voliccico  42161  stoweidlem1  42163  stoweidlem3  42165  stoweidlem7  42169  stoweidlem24  42186  stoweidlem26  42188  stoweidlem42  42204  wallispilem5  42231  stirlinglem1  42236  stirlinglem6  42241  stirlinglem7  42242  stirlinglem10  42245  stirlinglem12  42247  stirlinglem13  42248  stirlingr  42252  dirkertrigeqlem1  42260  fourierdlem10  42279  fourierdlem11  42280  fourierdlem12  42281  fourierdlem14  42283  fourierdlem15  42284  fourierdlem17  42286  fourierdlem19  42288  fourierdlem30  42299  fourierdlem37  42306  fourierdlem40  42309  fourierdlem41  42310  fourierdlem42  42311  fourierdlem47  42315  fourierdlem48  42316  fourierdlem49  42317  fourierdlem50  42318  fourierdlem51  42319  fourierdlem54  42322  fourierdlem63  42331  fourierdlem64  42332  fourierdlem65  42333  fourierdlem68  42336  fourierdlem73  42341  fourierdlem74  42342  fourierdlem76  42344  fourierdlem77  42345  fourierdlem78  42346  fourierdlem79  42347  fourierdlem81  42349  fourierdlem82  42350  fourierdlem83  42351  fourierdlem92  42360  fourierdlem93  42361  fourierdlem102  42370  fourierdlem103  42371  fourierdlem104  42372  fourierdlem107  42375  fourierdlem111  42379  fourierdlem114  42382  sqwvfoura  42390  sqwvfourb  42391  fouriersw  42393  etransclem19  42415  etransclem23  42419  etransclem35  42431  etransclem41  42437  qndenserrnbllem  42456  iundjiun  42619  carageniuncllem2  42681  caratheodorylem1  42685  hoicvr  42707  ovnsubaddlem1  42729  hsphoidmvle2  42744  hoidmv1lelem1  42750  hoidmv1lelem2  42751  hoidmvlelem1  42754  hoidmvlelem2  42755  hoidmvlelem3  42756  hoiqssbllem1  42781  hoiqssbllem2  42782  volico2  42800  iinhoiicclem  42832  iunhoiioolem  42834  vonioolem2  42840  vonicclem2  42843  pimdecfgtioo  42872  pimincfltioo  42873  smflimlem4  42927  smfmullem1  42943  smflimsuplem4  42974  expnegico01  44501  eenglngeehlnmlem2  44653  inlinecirc02plem  44701
  Copyright terms: Public domain W3C validator