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

Theorem ltled 10036
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 9977 . . 3 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵𝐴𝐵))
52, 3, 4syl2anc 690 . 2 (𝜑 → (𝐴 < 𝐵𝐴𝐵))
61, 5mpd 15 1 (𝜑𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1976   class class class wbr 4577  cr 9791   < clt 9930  cle 9931
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6824  ax-resscn 9849  ax-pre-lttri 9866
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-br 4578  df-opab 4638  df-mpt 4639  df-id 4943  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-er 7606  df-en 7819  df-dom 7820  df-sdom 7821  df-pnf 9932  df-mnf 9933  df-xr 9934  df-ltxr 9935  df-le 9936
This theorem is referenced by:  ltnsymd  10037  mulge0  10395  msqge0  10398  addgt0d  10451  lt2addd  10499  lt2msq1  10756  uzwo3  11615  fznatpl1  12220  flflp1  12425  modaddmodup  12550  expmulnbnd  12813  fzsdom2  13027  repswcshw  13355  isercolllem1  14189  caucvgrlem  14197  climcnds  14368  geomulcvg  14392  mertenslem1  14401  ruclem2  14746  ruclem12  14755  bitsfzo  14941  bitsmod  14942  lcmgcdlem  15103  isprm7  15204  4sqlem7  15432  vdwlem1  15469  met1stc  22077  cfilucfil  22115  nlmvscnlem2  22232  icccmplem2  22366  reconnlem2  22370  xrhmeo  22484  cnheibor  22493  nmoleub2lem3  22654  ipcnlem2  22769  minveclem3b  22924  ivthlem1  22944  ivthlem2  22945  ivth2  22948  ivthle  22949  ivthle2  22950  ovollb2lem  22980  ovolicc2lem4  23012  ovolicc2lem5  23013  ioombl1lem4  23053  uniioombllem4  23077  uniioombllem5  23078  opnmbllem  23092  ismbf3d  23144  mbfi1fseqlem6  23210  itg2gt0  23250  dveflem  23463  dvferm1lem  23468  dvferm2lem  23470  rollelem  23473  rolle  23474  cmvth  23475  mvth  23476  c1liplem1  23480  dvgt0lem1  23486  dvivthlem1  23492  lhop1lem  23497  lhop1  23498  dvcnvrelem1  23501  dvcnvrelem2  23502  dvcvx  23504  dgradd2  23745  aaliou3lem8  23821  aaliou3lem7  23825  ulmdvlem1  23875  itgulm  23883  radcnvlt1  23893  radcnvle  23895  abelthlem7  23913  efcvx  23924  coseq0negpitopi  23976  tangtx  23978  tanabsge  23979  tanord  24005  abslogimle  24041  divlogrlim  24098  logno1  24099  logcnlem3  24107  logcnlem4  24108  logtayl  24123  logccv  24126  cxple  24158  chordthmlem4  24279  asinsin  24336  atanlogaddlem  24357  atantan  24367  cxp2limlem  24419  logdifbnd  24437  emcllem4  24442  harmonicbnd4  24454  lgamucov  24481  ftalem1  24516  ftalem2  24517  ftalem3  24518  basellem5  24528  basellem8  24531  chpchtsum  24661  bposlem1  24726  lgseisenlem1  24817  lgsquadlem1  24822  lgsquadlem2  24823  lgsquadlem3  24824  chebbnd1lem2  24876  chebbnd1lem3  24877  chtppilimlem1  24879  chto1ub  24882  chpo1ubb  24887  vmadivsumb  24889  dchrisumlem3  24897  mulog2sumlem1  24940  vmalogdivsum2  24944  vmalogdivsum  24945  2vmadivsumlem  24946  selbergb  24955  selberg2b  24958  chpdifbndlem1  24959  selberg3lem2  24964  selberg3  24965  selberg4lem1  24966  selberg4  24967  pntrsumbnd  24972  selberg3r  24975  selberg4r  24976  selberg34r  24977  pntrlog2bndlem1  24983  pntrlog2bndlem2  24984  pntrlog2bndlem3  24985  pntrlog2bndlem4  24986  pntrlog2bndlem5  24987  pntrlog2bndlem6a  24988  pntrlog2bndlem6  24989  pntrlog2bnd  24990  pntpbnd1a  24991  pntpbnd1  24992  pntpbnd2  24993  pntibndlem2  24997  pntlemb  25003  pntlemq  25007  pntlemr  25008  pntlemj  25009  pntlemf  25011  pntlemp  25016  ostth2lem2  25040  axpaschlem  25538  axlowdimlem16  25555  smcnlem  26737  bcm1n  28747  smatrcl  28996  fiunelros  29370  dya2icoseg  29472  eulerpartlemgc  29557  dstfrvunirn  29669  ballotlemfc0  29687  ballotlemfcc  29688  ballotlemimin  29700  ballotlemsgt1  29705  ballotlemfrcn0  29724  sgnmul  29737  subfacval3  30231  erdszelem8  30240  cvmliftlem6  30332  cvmliftlem7  30333  cvmliftlem8  30334  cvmliftlem9  30335  cvmliftlem10  30336  sinccvglem  30626  dnibndlem9  31452  unbdqndv2lem2  31477  knoppndvlem14  31492  knoppndvlem18  31496  knoppndvlem19  31497  poimirlem7  32382  poimirlem15  32390  opnmbllem0  32411  itg2addnclem  32427  itg2addnclem3  32429  itg2addnc  32430  itg2gt0cn  32431  areacirclem1  32466  areacirc  32471  isbnd3  32549  cntotbnd  32561  rrnequiv  32600  irrapxlem3  36202  pellexlem2  36208  pellfundglb  36263  monotuz  36320  monotoddzzfi  36321  acongrep  36361  cvgdvgrat  37330  hashnzfz2  37338  hashnzfzclim  37339  binomcxplemnotnn0  37373  monoords  38248  xralrple2  38308  reclt0d  38345  reclt0  38352  iooiinicc  38413  iooiinioc  38427  limciccioolb  38485  limcicciooub  38501  lptre2pt  38504  icccncfext  38570  cncfiooicclem1  38576  dvdivbd  38610  dvbdfbdioolem1  38615  dvbdfbdioolem2  38616  ioodvbdlimc1lem2  38619  ioodvbdlimc2lem  38621  dvnxpaek  38629  dvnmul  38630  volioc  38661  iblspltprt  38662  itgspltprt  38668  volico  38673  volioore  38680  voliooico  38682  voliccico  38689  stoweidlem1  38691  stoweidlem3  38693  stoweidlem7  38697  stoweidlem24  38714  stoweidlem26  38716  stoweidlem42  38732  wallispilem5  38759  stirlinglem1  38764  stirlinglem6  38769  stirlinglem7  38770  stirlinglem10  38773  stirlinglem12  38775  stirlinglem13  38776  stirlingr  38780  dirkertrigeqlem1  38788  fourierdlem10  38807  fourierdlem11  38808  fourierdlem12  38809  fourierdlem14  38811  fourierdlem15  38812  fourierdlem17  38814  fourierdlem19  38816  fourierdlem30  38827  fourierdlem37  38834  fourierdlem40  38837  fourierdlem41  38838  fourierdlem42  38839  fourierdlem47  38843  fourierdlem48  38844  fourierdlem49  38845  fourierdlem50  38846  fourierdlem51  38847  fourierdlem54  38850  fourierdlem63  38859  fourierdlem64  38860  fourierdlem65  38861  fourierdlem68  38864  fourierdlem73  38869  fourierdlem74  38870  fourierdlem76  38872  fourierdlem77  38873  fourierdlem78  38874  fourierdlem79  38875  fourierdlem81  38877  fourierdlem82  38878  fourierdlem83  38879  fourierdlem92  38888  fourierdlem93  38889  fourierdlem102  38898  fourierdlem103  38899  fourierdlem104  38900  fourierdlem107  38903  fourierdlem111  38907  fourierdlem114  38910  sqwvfoura  38918  sqwvfourb  38919  fouriersw  38921  etransclem19  38943  etransclem23  38947  etransclem35  38959  etransclem41  38965  qndenserrnbllem  38987  iundjiun  39150  carageniuncllem2  39209  caratheodorylem1  39213  hoicvr  39235  ovnsubaddlem1  39257  hsphoidmvle2  39272  hoidmv1lelem1  39278  hoidmv1lelem2  39279  hoidmvlelem1  39282  hoidmvlelem2  39283  hoidmvlelem3  39284  hoiqssbllem1  39309  hoiqssbllem2  39310  volico2  39328  iinhoiicclem  39361  iunhoiioolem  39363  vonioolem2  39369  vonicclem2  39372  pimdecfgtioo  39401  pimincfltioo  39402  smflimlem4  39457  smfmullem1  39473  expnegico01  42097
  Copyright terms: Public domain W3C validator