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

Theorem ltled 10377
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 10318 . . 3 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵𝐴𝐵))
52, 3, 4syl2anc 696 . 2 (𝜑 → (𝐴 < 𝐵𝐴𝐵))
61, 5mpd 15 1 (𝜑𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2139   class class class wbr 4804  cr 10127   < clt 10266  cle 10267
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114  ax-resscn 10185  ax-pre-lttri 10202
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-nel 3036  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-br 4805  df-opab 4865  df-mpt 4882  df-id 5174  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-er 7911  df-en 8122  df-dom 8123  df-sdom 8124  df-pnf 10268  df-mnf 10269  df-xr 10270  df-ltxr 10271  df-le 10272
This theorem is referenced by:  ltnsymd  10378  mulge0  10738  msqge0  10741  addgt0d  10794  lt2addd  10842  lt2msq1  11099  uzwo3  11976  fznatpl1  12588  flflp1  12802  modaddmodup  12927  expmulnbnd  13190  fzsdom2  13407  repswcshw  13758  isercolllem1  14594  caucvgrlem  14602  climcnds  14782  geomulcvg  14806  mertenslem1  14815  ruclem2  15160  ruclem12  15169  bitsfzo  15359  bitsmod  15360  lcmgcdlem  15521  isprm7  15622  4sqlem7  15850  vdwlem1  15887  met1stc  22527  cfilucfil  22565  nlmvscnlem2  22690  icccmplem2  22827  reconnlem2  22831  xrhmeo  22946  cnheibor  22955  nmoleub2lem3  23115  ipcnlem2  23243  minveclem3b  23399  ivthlem1  23420  ivthlem2  23421  ivth2  23424  ivthle  23425  ivthle2  23426  ovollb2lem  23456  ovolicc2lem4  23488  ovolicc2lem5  23489  ioombl1lem4  23529  uniioombllem4  23554  uniioombllem5  23555  opnmbllem  23569  ismbf3d  23620  mbfi1fseqlem6  23686  itg2gt0  23726  dveflem  23941  dvferm1lem  23946  dvferm2lem  23948  rollelem  23951  rolle  23952  cmvth  23953  mvth  23954  c1liplem1  23958  dvgt0lem1  23964  dvivthlem1  23970  lhop1lem  23975  lhop1  23976  dvcnvrelem1  23979  dvcnvrelem2  23980  dvcvx  23982  dgradd2  24223  aaliou3lem8  24299  aaliou3lem7  24303  ulmdvlem1  24353  itgulm  24361  radcnvlt1  24371  radcnvle  24373  abelthlem7  24391  efcvx  24402  coseq0negpitopi  24454  tangtx  24456  tanabsge  24457  tanord  24483  abslogimle  24519  divlogrlim  24580  logno1  24581  logcnlem3  24589  logcnlem4  24590  logtayl  24605  logccv  24608  cxple  24640  chordthmlem4  24761  asinsin  24818  atanlogaddlem  24839  atantan  24849  cxp2limlem  24901  logdifbnd  24919  emcllem4  24924  harmonicbnd4  24936  lgamucov  24963  ftalem1  24998  ftalem2  24999  ftalem3  25000  basellem5  25010  basellem8  25013  chpchtsum  25143  bposlem1  25208  lgseisenlem1  25299  lgsquadlem1  25304  lgsquadlem2  25305  lgsquadlem3  25306  chebbnd1lem2  25358  chebbnd1lem3  25359  chtppilimlem1  25361  chto1ub  25364  chpo1ubb  25369  vmadivsumb  25371  dchrisumlem3  25379  mulog2sumlem1  25422  vmalogdivsum2  25426  vmalogdivsum  25427  2vmadivsumlem  25428  selbergb  25437  selberg2b  25440  chpdifbndlem1  25441  selberg3lem2  25446  selberg3  25447  selberg4lem1  25448  selberg4  25449  pntrsumbnd  25454  selberg3r  25457  selberg4r  25458  selberg34r  25459  pntrlog2bndlem1  25465  pntrlog2bndlem2  25466  pntrlog2bndlem3  25467  pntrlog2bndlem4  25468  pntrlog2bndlem5  25469  pntrlog2bndlem6a  25470  pntrlog2bndlem6  25471  pntrlog2bnd  25472  pntpbnd1a  25473  pntpbnd1  25474  pntpbnd2  25475  pntibndlem2  25479  pntlemb  25485  pntlemq  25489  pntlemr  25490  pntlemj  25491  pntlemf  25493  pntlemp  25498  ostth2lem2  25522  axpaschlem  26019  axlowdimlem16  26036  smcnlem  27861  bcm1n  29863  smatrcl  30171  fiunelros  30546  dya2icoseg  30648  eulerpartlemgc  30733  dstfrvunirn  30845  ballotlemfc0  30863  ballotlemfcc  30864  ballotlemimin  30876  ballotlemsgt1  30881  ballotlemfrcn0  30900  sgnmul  30913  fdvposlt  30986  breprexp  31020  logdivsqrle  31037  hgt750leme  31045  tgoldbachgt  31050  subfacval3  31478  erdszelem8  31487  cvmliftlem6  31579  cvmliftlem7  31580  cvmliftlem8  31581  cvmliftlem9  31582  cvmliftlem10  31583  sinccvglem  31873  dnibndlem9  32782  unbdqndv2lem2  32807  knoppndvlem14  32822  knoppndvlem18  32826  knoppndvlem19  32827  poimirlem7  33729  poimirlem15  33737  opnmbllem0  33758  itg2addnclem  33774  itg2addnclem3  33776  itg2addnc  33777  itg2gt0cn  33778  areacirclem1  33813  areacirc  33818  isbnd3  33896  cntotbnd  33908  rrnequiv  33947  irrapxlem3  37890  pellexlem2  37896  pellfundglb  37951  monotuz  38008  monotoddzzfi  38009  acongrep  38049  cvgdvgrat  39014  hashnzfz2  39022  hashnzfzclim  39023  binomcxplemnotnn0  39057  monoords  40010  xralrple2  40068  reclt0d  40105  reclt0  40112  uzublem  40155  iooiinicc  40272  iooiinioc  40286  limciccioolb  40356  limcicciooub  40372  lptre2pt  40375  limsupubuzlem  40447  limsup10exlem  40507  icccncfext  40603  cncfiooicclem1  40609  dvdivbd  40641  dvbdfbdioolem1  40646  dvbdfbdioolem2  40647  ioodvbdlimc1lem2  40650  ioodvbdlimc2lem  40652  dvnxpaek  40660  dvnmul  40661  volioc  40691  iblspltprt  40692  itgspltprt  40698  volico  40703  volioore  40710  voliooico  40712  voliccico  40719  stoweidlem1  40721  stoweidlem3  40723  stoweidlem7  40727  stoweidlem24  40744  stoweidlem26  40746  stoweidlem42  40762  wallispilem5  40789  stirlinglem1  40794  stirlinglem6  40799  stirlinglem7  40800  stirlinglem10  40803  stirlinglem12  40805  stirlinglem13  40806  stirlingr  40810  dirkertrigeqlem1  40818  fourierdlem10  40837  fourierdlem11  40838  fourierdlem12  40839  fourierdlem14  40841  fourierdlem15  40842  fourierdlem17  40844  fourierdlem19  40846  fourierdlem30  40857  fourierdlem37  40864  fourierdlem40  40867  fourierdlem41  40868  fourierdlem42  40869  fourierdlem47  40873  fourierdlem48  40874  fourierdlem49  40875  fourierdlem50  40876  fourierdlem51  40877  fourierdlem54  40880  fourierdlem63  40889  fourierdlem64  40890  fourierdlem65  40891  fourierdlem68  40894  fourierdlem73  40899  fourierdlem74  40900  fourierdlem76  40902  fourierdlem77  40903  fourierdlem78  40904  fourierdlem79  40905  fourierdlem81  40907  fourierdlem82  40908  fourierdlem83  40909  fourierdlem92  40918  fourierdlem93  40919  fourierdlem102  40928  fourierdlem103  40929  fourierdlem104  40930  fourierdlem107  40933  fourierdlem111  40937  fourierdlem114  40940  sqwvfoura  40948  sqwvfourb  40949  fouriersw  40951  etransclem19  40973  etransclem23  40977  etransclem35  40989  etransclem41  40995  qndenserrnbllem  41017  iundjiun  41180  carageniuncllem2  41242  caratheodorylem1  41246  hoicvr  41268  ovnsubaddlem1  41290  hsphoidmvle2  41305  hoidmv1lelem1  41311  hoidmv1lelem2  41312  hoidmvlelem1  41315  hoidmvlelem2  41316  hoidmvlelem3  41317  hoiqssbllem1  41342  hoiqssbllem2  41343  volico2  41361  iinhoiicclem  41393  iunhoiioolem  41395  vonioolem2  41401  vonicclem2  41404  pimdecfgtioo  41433  pimincfltioo  41434  smflimlem4  41488  smfmullem1  41504  smflimsuplem4  41535  expnegico01  42818
  Copyright terms: Public domain W3C validator