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

Theorem ltled 10223
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 10164 . . 3 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵𝐴𝐵))
52, 3, 4syl2anc 694 . 2 (𝜑 → (𝐴 < 𝐵𝐴𝐵))
61, 5mpd 15 1 (𝜑𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2030   class class class wbr 4685  cr 9973   < clt 10112  cle 10113
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-resscn 10031  ax-pre-lttri 10048
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-er 7787  df-en 7998  df-dom 7999  df-sdom 8000  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118
This theorem is referenced by:  ltnsymd  10224  mulge0  10584  msqge0  10587  addgt0d  10640  lt2addd  10688  lt2msq1  10945  uzwo3  11821  fznatpl1  12433  flflp1  12648  modaddmodup  12773  expmulnbnd  13036  fzsdom2  13253  repswcshw  13604  isercolllem1  14439  caucvgrlem  14447  climcnds  14627  geomulcvg  14651  mertenslem1  14660  ruclem2  15005  ruclem12  15014  bitsfzo  15204  bitsmod  15205  lcmgcdlem  15366  isprm7  15467  4sqlem7  15695  vdwlem1  15732  met1stc  22373  cfilucfil  22411  nlmvscnlem2  22536  icccmplem2  22673  reconnlem2  22677  xrhmeo  22792  cnheibor  22801  nmoleub2lem3  22961  ipcnlem2  23089  minveclem3b  23245  ivthlem1  23266  ivthlem2  23267  ivth2  23270  ivthle  23271  ivthle2  23272  ovollb2lem  23302  ovolicc2lem4  23334  ovolicc2lem5  23335  ioombl1lem4  23375  uniioombllem4  23400  uniioombllem5  23401  opnmbllem  23415  ismbf3d  23466  mbfi1fseqlem6  23532  itg2gt0  23572  dveflem  23787  dvferm1lem  23792  dvferm2lem  23794  rollelem  23797  rolle  23798  cmvth  23799  mvth  23800  c1liplem1  23804  dvgt0lem1  23810  dvivthlem1  23816  lhop1lem  23821  lhop1  23822  dvcnvrelem1  23825  dvcnvrelem2  23826  dvcvx  23828  dgradd2  24069  aaliou3lem8  24145  aaliou3lem7  24149  ulmdvlem1  24199  itgulm  24207  radcnvlt1  24217  radcnvle  24219  abelthlem7  24237  efcvx  24248  coseq0negpitopi  24300  tangtx  24302  tanabsge  24303  tanord  24329  abslogimle  24365  divlogrlim  24426  logno1  24427  logcnlem3  24435  logcnlem4  24436  logtayl  24451  logccv  24454  cxple  24486  chordthmlem4  24607  asinsin  24664  atanlogaddlem  24685  atantan  24695  cxp2limlem  24747  logdifbnd  24765  emcllem4  24770  harmonicbnd4  24782  lgamucov  24809  ftalem1  24844  ftalem2  24845  ftalem3  24846  basellem5  24856  basellem8  24859  chpchtsum  24989  bposlem1  25054  lgseisenlem1  25145  lgsquadlem1  25150  lgsquadlem2  25151  lgsquadlem3  25152  chebbnd1lem2  25204  chebbnd1lem3  25205  chtppilimlem1  25207  chto1ub  25210  chpo1ubb  25215  vmadivsumb  25217  dchrisumlem3  25225  mulog2sumlem1  25268  vmalogdivsum2  25272  vmalogdivsum  25273  2vmadivsumlem  25274  selbergb  25283  selberg2b  25286  chpdifbndlem1  25287  selberg3lem2  25292  selberg3  25293  selberg4lem1  25294  selberg4  25295  pntrsumbnd  25300  selberg3r  25303  selberg4r  25304  selberg34r  25305  pntrlog2bndlem1  25311  pntrlog2bndlem2  25312  pntrlog2bndlem3  25313  pntrlog2bndlem4  25314  pntrlog2bndlem5  25315  pntrlog2bndlem6a  25316  pntrlog2bndlem6  25317  pntrlog2bnd  25318  pntpbnd1a  25319  pntpbnd1  25320  pntpbnd2  25321  pntibndlem2  25325  pntlemb  25331  pntlemq  25335  pntlemr  25336  pntlemj  25337  pntlemf  25339  pntlemp  25344  ostth2lem2  25368  axpaschlem  25865  axlowdimlem16  25882  smcnlem  27680  bcm1n  29682  smatrcl  29990  fiunelros  30365  dya2icoseg  30467  eulerpartlemgc  30552  dstfrvunirn  30664  ballotlemfc0  30682  ballotlemfcc  30683  ballotlemimin  30695  ballotlemsgt1  30700  ballotlemfrcn0  30719  sgnmul  30732  fdvposlt  30805  breprexp  30839  logdivsqrle  30856  hgt750leme  30864  tgoldbachgt  30869  subfacval3  31297  erdszelem8  31306  cvmliftlem6  31398  cvmliftlem7  31399  cvmliftlem8  31400  cvmliftlem9  31401  cvmliftlem10  31402  sinccvglem  31692  dnibndlem9  32601  unbdqndv2lem2  32626  knoppndvlem14  32641  knoppndvlem18  32645  knoppndvlem19  32646  poimirlem7  33546  poimirlem15  33554  opnmbllem0  33575  itg2addnclem  33591  itg2addnclem3  33593  itg2addnc  33594  itg2gt0cn  33595  areacirclem1  33630  areacirc  33635  isbnd3  33713  cntotbnd  33725  rrnequiv  33764  irrapxlem3  37705  pellexlem2  37711  pellfundglb  37766  monotuz  37823  monotoddzzfi  37824  acongrep  37864  cvgdvgrat  38829  hashnzfz2  38837  hashnzfzclim  38838  binomcxplemnotnn0  38872  monoords  39825  xralrple2  39883  reclt0d  39920  reclt0  39927  uzublem  39970  iooiinicc  40087  iooiinioc  40101  limciccioolb  40171  limcicciooub  40187  lptre2pt  40190  limsupubuzlem  40262  limsup10exlem  40322  icccncfext  40418  cncfiooicclem1  40424  dvdivbd  40456  dvbdfbdioolem1  40461  dvbdfbdioolem2  40462  ioodvbdlimc1lem2  40465  ioodvbdlimc2lem  40467  dvnxpaek  40475  dvnmul  40476  volioc  40506  iblspltprt  40507  itgspltprt  40513  volico  40518  volioore  40525  voliooico  40527  voliccico  40534  stoweidlem1  40536  stoweidlem3  40538  stoweidlem7  40542  stoweidlem24  40559  stoweidlem26  40561  stoweidlem42  40577  wallispilem5  40604  stirlinglem1  40609  stirlinglem6  40614  stirlinglem7  40615  stirlinglem10  40618  stirlinglem12  40620  stirlinglem13  40621  stirlingr  40625  dirkertrigeqlem1  40633  fourierdlem10  40652  fourierdlem11  40653  fourierdlem12  40654  fourierdlem14  40656  fourierdlem15  40657  fourierdlem17  40659  fourierdlem19  40661  fourierdlem30  40672  fourierdlem37  40679  fourierdlem40  40682  fourierdlem41  40683  fourierdlem42  40684  fourierdlem47  40688  fourierdlem48  40689  fourierdlem49  40690  fourierdlem50  40691  fourierdlem51  40692  fourierdlem54  40695  fourierdlem63  40704  fourierdlem64  40705  fourierdlem65  40706  fourierdlem68  40709  fourierdlem73  40714  fourierdlem74  40715  fourierdlem76  40717  fourierdlem77  40718  fourierdlem78  40719  fourierdlem79  40720  fourierdlem81  40722  fourierdlem82  40723  fourierdlem83  40724  fourierdlem92  40733  fourierdlem93  40734  fourierdlem102  40743  fourierdlem103  40744  fourierdlem104  40745  fourierdlem107  40748  fourierdlem111  40752  fourierdlem114  40755  sqwvfoura  40763  sqwvfourb  40764  fouriersw  40766  etransclem19  40788  etransclem23  40792  etransclem35  40804  etransclem41  40810  qndenserrnbllem  40832  iundjiun  40995  carageniuncllem2  41057  caratheodorylem1  41061  hoicvr  41083  ovnsubaddlem1  41105  hsphoidmvle2  41120  hoidmv1lelem1  41126  hoidmv1lelem2  41127  hoidmvlelem1  41130  hoidmvlelem2  41131  hoidmvlelem3  41132  hoiqssbllem1  41157  hoiqssbllem2  41158  volico2  41176  iinhoiicclem  41208  iunhoiioolem  41210  vonioolem2  41216  vonicclem2  41219  pimdecfgtioo  41248  pimincfltioo  41249  smflimlem4  41303  smfmullem1  41319  smflimsuplem4  41350  expnegico01  42633
  Copyright terms: Public domain W3C validator