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

Theorem ltled 11302
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 11242 . . 3 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵𝐴𝐵))
52, 3, 4syl2anc 584 . 2 (𝜑 → (𝐴 < 𝐵𝐴𝐵))
61, 5mpd 15 1 (𝜑𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2106   class class class wbr 5105  cr 11049   < clt 11188  cle 11189
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7671  ax-resscn 11107  ax-pre-lttri 11124
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-br 5106  df-opab 5168  df-mpt 5189  df-id 5531  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-er 8647  df-en 8883  df-dom 8884  df-sdom 8885  df-pnf 11190  df-mnf 11191  df-xr 11192  df-ltxr 11193  df-le 11194
This theorem is referenced by:  ltnsymd  11303  mulge0  11672  msqge0  11675  addgt0d  11729  lt2addd  11777  lt2msq1  12038  uzwo3  12867  fznatpl1  13494  flflp1  13711  modaddmodup  13838  expmulnbnd  14137  fzsdom2  14327  repswcshw  14699  isercolllem1  15548  caucvgrlem  15556  climcnds  15735  geomulcvg  15760  mertenslem1  15768  ruclem2  16113  ruclem12  16122  bitsfzo  16314  bitsmod  16315  lcmgcdlem  16481  isprm7  16583  4sqlem7  16815  vdwlem1  16852  met1stc  23875  cfilucfil  23913  nlmvscnlem2  24047  icccmplem2  24184  reconnlem2  24188  xrhmeo  24307  cnheibor  24316  nmoleub2lem3  24476  ipcnlem2  24606  minveclem3b  24790  ivthlem1  24813  ivthlem2  24814  ivth2  24817  ivthle  24818  ivthle2  24819  ovollb2lem  24850  ovolicc2lem4  24882  ovolicc2lem5  24883  ioombl1lem4  24923  uniioombllem4  24948  uniioombllem5  24949  opnmbllem  24963  ismbf3d  25016  mbfi1fseqlem6  25083  itg2gt0  25123  dveflem  25341  dvferm1lem  25346  dvferm2lem  25348  rollelem  25351  rolle  25352  cmvth  25353  mvth  25354  c1liplem1  25358  dvgt0lem1  25364  dvivthlem1  25370  lhop1lem  25375  lhop1  25376  dvcnvrelem1  25379  dvcnvrelem2  25380  dvcvx  25382  dgradd2  25627  aaliou3lem8  25703  aaliou3lem7  25707  ulmdvlem1  25757  itgulm  25765  radcnvlt1  25775  radcnvle  25777  abelthlem7  25795  efcvx  25806  coseq0negpitopi  25858  tangtx  25860  tanabsge  25861  tanord  25892  abslogimle  25927  divlogrlim  25988  logno1  25989  logcnlem3  25997  logcnlem4  25998  logtayl  26013  logccv  26016  cxple  26048  chordthmlem4  26183  asinsin  26240  atanlogaddlem  26261  atantan  26271  cxp2limlem  26323  logdifbnd  26341  emcllem4  26346  harmonicbnd4  26358  lgamucov  26385  ftalem1  26420  ftalem2  26421  ftalem3  26422  basellem5  26432  basellem8  26435  chpchtsum  26565  bposlem1  26630  lgseisenlem1  26721  lgsquadlem1  26726  lgsquadlem2  26727  lgsquadlem3  26728  2sqreulem1  26792  2sqreunnlem1  26795  chebbnd1lem2  26816  chebbnd1lem3  26817  chtppilimlem1  26819  chto1ub  26822  chpo1ubb  26827  vmadivsumb  26829  dchrisumlem3  26837  mulog2sumlem1  26880  vmalogdivsum2  26884  vmalogdivsum  26885  2vmadivsumlem  26886  selbergb  26895  selberg2b  26898  chpdifbndlem1  26899  selberg3lem2  26904  selberg3  26905  selberg4lem1  26906  selberg4  26907  pntrsumbnd  26912  selberg3r  26915  selberg4r  26916  selberg34r  26917  pntrlog2bndlem1  26923  pntrlog2bndlem2  26924  pntrlog2bndlem3  26925  pntrlog2bndlem4  26926  pntrlog2bndlem5  26927  pntrlog2bndlem6a  26928  pntrlog2bndlem6  26929  pntrlog2bnd  26930  pntpbnd1a  26931  pntpbnd1  26932  pntpbnd2  26933  pntibndlem2  26937  pntlemb  26943  pntlemq  26947  pntlemr  26948  pntlemj  26949  pntlemf  26951  pntlemp  26956  ostth2lem2  26980  axpaschlem  27887  axlowdimlem16  27904  smcnlem  29637  bcm1n  31693  wrdt2ind  31802  cycpmco2lem6  31975  cyc3conja  32001  smatrcl  32368  fiunelros  32764  dya2icoseg  32868  eulerpartlemgc  32953  dstfrvunirn  33065  ballotlemfc0  33083  ballotlemfcc  33084  ballotlemimin  33096  ballotlemsgt1  33101  ballotlemfrcn0  33120  sgnmul  33133  fdvposlt  33203  breprexp  33237  logdivsqrle  33254  hgt750leme  33262  tgoldbachgt  33267  lpadmax  33286  lpadright  33288  subfacval3  33774  erdszelem8  33783  cvmliftlem6  33875  cvmliftlem7  33876  cvmliftlem8  33877  cvmliftlem9  33878  cvmliftlem10  33879  sinccvglem  34251  dnibndlem9  34940  unbdqndv2lem2  34964  knoppndvlem14  34979  knoppndvlem18  34983  knoppndvlem19  34984  poimirlem7  36076  poimirlem15  36084  opnmbllem0  36105  itg2addnclem  36120  itg2addnclem3  36122  itg2addnc  36123  itg2gt0cn  36124  areacirclem1  36157  areacirc  36162  isbnd3  36234  cntotbnd  36246  rrnequiv  36285  lcmineqlem11  40487  lcmineqlem22  40498  3lexlogpow5ineq2  40503  3lexlogpow5ineq5  40508  dvrelogpow2b  40516  aks4d1p1p2  40518  aks4d1p1p4  40519  aks4d1p1p6  40521  aks4d1p1p7  40522  aks4d1p1p5  40523  aks4d1p1  40524  aks4d1p2  40525  aks4d1p3  40526  aks4d1p5  40528  aks4d1p7d1  40530  aks4d1p7  40531  aks4d1p8  40535  sticksstones6  40550  sticksstones12a  40556  sticksstones12  40557  metakunt7  40574  metakunt29  40596  metakunt30  40597  nn0rppwr  40797  nn0expgcd  40799  posqsqznn  40807  rtprmirr  40811  fltnltalem  40978  irrapxlem3  41125  pellexlem2  41131  pellfundglb  41186  monotuz  41243  monotoddzzfi  41244  acongrep  41282  cvgdvgrat  42575  hashnzfz2  42583  hashnzfzclim  42584  binomcxplemnotnn0  42618  monoords  43507  xralrple2  43564  reclt0d  43597  reclt0  43602  uzublem  43641  iooiinicc  43752  iooiinioc  43766  limciccioolb  43834  limcicciooub  43850  lptre2pt  43853  limsupubuzlem  43925  limsup10exlem  43985  icccncfext  44100  cncfiooicclem1  44106  dvdivbd  44136  dvbdfbdioolem1  44141  dvbdfbdioolem2  44142  ioodvbdlimc1lem2  44145  ioodvbdlimc2lem  44147  dvnxpaek  44155  dvnmul  44156  volioc  44185  iblspltprt  44186  itgspltprt  44192  volico  44196  volioore  44203  voliooico  44205  voliccico  44212  stoweidlem1  44214  stoweidlem3  44216  stoweidlem7  44220  stoweidlem24  44237  stoweidlem26  44239  stoweidlem42  44255  wallispilem5  44282  stirlinglem1  44287  stirlinglem6  44292  stirlinglem7  44293  stirlinglem10  44296  stirlinglem12  44298  stirlinglem13  44299  stirlingr  44303  dirkertrigeqlem1  44311  fourierdlem10  44330  fourierdlem11  44331  fourierdlem12  44332  fourierdlem14  44334  fourierdlem15  44335  fourierdlem17  44337  fourierdlem19  44339  fourierdlem30  44350  fourierdlem37  44357  fourierdlem40  44360  fourierdlem41  44361  fourierdlem42  44362  fourierdlem47  44366  fourierdlem48  44367  fourierdlem49  44368  fourierdlem50  44369  fourierdlem51  44370  fourierdlem54  44373  fourierdlem63  44382  fourierdlem64  44383  fourierdlem65  44384  fourierdlem68  44387  fourierdlem73  44392  fourierdlem74  44393  fourierdlem76  44395  fourierdlem77  44396  fourierdlem78  44397  fourierdlem79  44398  fourierdlem81  44400  fourierdlem82  44401  fourierdlem83  44402  fourierdlem92  44411  fourierdlem93  44412  fourierdlem102  44421  fourierdlem103  44422  fourierdlem104  44423  fourierdlem107  44426  fourierdlem111  44430  fourierdlem114  44433  sqwvfoura  44441  sqwvfourb  44442  fouriersw  44444  etransclem19  44466  etransclem23  44470  etransclem35  44482  etransclem41  44488  qndenserrnbllem  44507  iundjiun  44673  carageniuncllem2  44735  caratheodorylem1  44739  hoicvr  44761  ovnsubaddlem1  44783  hsphoidmvle2  44798  hoidmv1lelem1  44804  hoidmv1lelem2  44805  hoidmvlelem1  44808  hoidmvlelem2  44809  hoidmvlelem3  44810  hoiqssbllem1  44835  hoiqssbllem2  44836  volico2  44854  iinhoiicclem  44886  iunhoiioolem  44888  vonioolem2  44894  vonicclem2  44897  pimdecfgtioo  44930  pimincfltioo  44931  smflimlem4  44987  smfmullem1  45004  smflimsuplem4  45036  expnegico01  46571  eenglngeehlnmlem2  46796  inlinecirc02plem  46844
  Copyright terms: Public domain W3C validator