Theorem elfzelz 13663

Description: A member of a finite set of sequential integers is an integer. (Contributed by NM, 6-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)

Assertion

Ref	Expression
elfzelz	⊢ (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ ℤ)

Proof of Theorem elfzelz

Step	Hyp	Ref	Expression
1		elfzuz 13659	. 2 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ (ℤ≥‘𝑀))
2		eluzelz 12982	. 2 ⊢ (𝐾 ∈ (ℤ≥‘𝑀) → 𝐾 ∈ ℤ)
3	1, 2	syl 18	1 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ ℤ)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  ‘cfv 6543  (class class class)co 7424  ℤcz 12700  ℤ_≥cuz 12972  ...cfz 13646

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5391  ax-un 7755  ax-cnex 11263  ax-resscn 11264

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3848  df-ss 3897  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6497  df-fun 6545  df-fn 6546  df-f 6547  df-fv 6551  df-ov 7427  df-oprab 7428  df-mpo 7429  df-1st 8005  df-2nd 8006  df-neg 11551  df-z 12701  df-uz 12973  df-fz 13647

This theorem is used by:  elfzelzd  13664  fzssz  13665  elfz1eq  13675  fzsplit2  13690  fzdisj  13692  elfznn  13694  ssfzunsnext  13710  fznatpl1  13719  fzrev2i  13730  fzrev3i  13732  fznuz  13750  fzrevral  13753  fzshftral  13756  fznn0sub2  13776  elfzmlbm  13779  difelfznle  13783  predfz  13794  fzosplit  13834  sermono  14184  seqf1olem1  14191  seqf1olem2  14192  bcval2  14456  bcval4  14458  bccmpl  14460  bcp1nk  14468  bcval5  14469  bcpasc  14472  bccl2  14474  seqcoll2  14617  swrdval2  14802  swrdwrdsymb  14820  ccatpfx  14858  swrdswrd  14862  swrdpfx  14864  pfxccatin12lem2a  14884  pfxccatin12lem1  14885  swrdccatin2  14886  pfxccatin12lem2  14888  pfxccatin12  14890  spllen  14911  revpfxsfxrev  14925  swrdrevpfx  14926  cshwidxm  14967  cshwidxn  14968  lswcshw  14974  2cshwcshw  14984  cshwcshid  14986  cshwcsh2id  14987  swrds2m  15101  seqshft  15247  sumrblem  15886  summolem2a  15890  fsum0diaglem  15951  mptfzshft  15953  fsumshftm  15956  fsum0diag2  15958  binomlem  16007  binom11  16010  bcxmas  16013  arisum  16038  geo2sum  16051  mertenslem1  16062  prodfn0  16072  prodrblem  16105  prodmolem2a  16110  fprodntriv  16118  fprodser  16125  fprodrev  16153  fallfacval3  16188  fallfacfwd  16211  0fallfac  16212  binomfallfaclem1  16214  binomfallfaclem2  16215  binomrisefac  16217  fallfacval4  16218  bpolycl  16227  bpolysum  16228  bpolydiflem  16229  fsumkthpow  16231  bpoly4  16234  fzm1ndvds  16501  pwp1fsum  16570  prmdvdsfz  16890  isprm7  16893  prmdvdsbc  16911  hashdvds  16961  phiprmpw  16962  prmdiveq  16972  modprminv  16986  modprminveq  16987  modprm0  16992  4sqlem11  17142  vdwapun  17161  prmop1  17225  prmdvdsprmo  17229  prmdvdsprmop  17230  prmgaplem1  17236  prmgaplem2  17237  prmgaplcmlem1  17238  prmgaplcmlem2  17239  prmgapprmo  17249  cshwshashlem1  17282  cshwshashlem2  17283  dfod2  19787  gsummptshft  20159  srgbinomlem3  20463  srgbinomlem4  20464  srgbinomlem  20465  freshmansdream  21889  chpscmatgsummon  23172  cayhamlem1  23193  iscmet3  25623  mbfi1fseqlem4  26048  itgz  26110  itgcl  26113  ibl0  26116  iblss  26134  iblss2  26135  itgss  26141  itgeqa  26143  iblconst  26147  iblabsr  26159  iblmulc2  26160  itgsplit  26165  dvfsumlem3  26357  plyeq0lem  26538  aalioulem1  26668  cxpeq  27094  birthdaylem2  27289  wilthlem1  27404  wilthlem3  27406  ftalem5  27413  basellem3  27419  basellem4  27420  dvdsppwf1o  27522  dvdsflf1o  27523  musum  27527  ppiub  27540  chtublem  27547  mersenne  27563  bposlem1  27620  lgsval2lem  27643  lgsdilem2  27669  lgsqrlem2  27683  gausslemma2dlem1a  27701  gausslemma2dlem1  27702  gausslemma2dlem3  27704  gausslemma2dlem4  27705  gausslemma2dlem5a  27706  gausslemma2dlem5  27707  gausslemma2dlem6  27708  lgseisenlem1  27711  lgseisenlem2  27712  lgseisenlem3  27713  lgsquadlem1  27716  lgsquadlem2  27717  lgsquadlem3  27718  2lgslem1a1  27725  2lgslem1a  27727  2lgslem1b  27728  rpvmasumlem  27823  dchrisumlem1  27825  dchrisumlem2  27826  dchrmusum2  27830  dchrvmasumlem1  27831  dchrvmasum2lem  27832  dchrvmasum2if  27833  dchrvmasumlem3  27835  dchrvmasumiflem1  27837  dchrvmasumiflem2  27838  dchrisum0flblem1  27844  rpvmasum2  27848  dchrisum0lem1b  27851  dchrisum0lem1  27852  dchrisum0lem2a  27853  dchrisum0lem2  27854  dchrisum0lem3  27855  dchrmusumlem  27858  dchrvmasumlem  27859  logdivbnd  27892  pntpbnd1  27922  pntlemh  27935  pntlemf  27941  ostth2lem2  27970  axlowdimlem13  29541  axlowdimlem14  29542  axlowdimlem16  29544  pfxwlk  30275  swrdwlk  30277  crctcshlem4  30418  crctcshwlkn0  30419  erclwwlkeqlen  30619  clwwnisshclwwsn  30659  eleclclwwlknlem2  30661  erclwwlkneqlen  30668  fzm1ne1  33430  fzsplit3  33435  bcm1n  33437  ballotlemfc0  35175  ballotlemfcc  35176  ballotlemodife  35180  ballotlemimin  35188  ballotlemsgt1  35193  ballotlemsel1i  35195  ballotlemsf1o  35196  ballotlemsi  35197  ballotlemsima  35198  ballotlemfg  35208  ballotlemfrc  35209  ballotlemfrcn0  35212  erdszelem8  36053  erdszelem9  36054  cvmliftlem7  36146  supfz  36590  inffz  36591  bcprod  36599  fwddifnp1  37026  poimirlem1  38648  poimirlem14  38661  poimirlem15  38662  poimirlem16  38663  poimirlem17  38664  poimirlem19  38666  poimirlem20  38667  poimirlem23  38670  poimirlem24  38671  poimirlem27  38674  poimirlem31  38678  poimirlem32  38679  mblfinlem2  38685  iblmulc2nc  38712  fdc  38788  lcmineqlem1  43188  lcmineqlem6  43193  lcmineqlem17  43204  aks4d1p1p1  43222  aks6d1c1  43275  hashscontpow  43281  aks6d1c5lem0  43294  aks6d1c5lem3  43296  aks6d1c5  43298  sticksstones6  43310  sticksstones7  43311  sticksstones10  43314  sticksstones12a  43316  sticksstones12  43317  aks6d1c6lem1  43329  bcled  43337  bcle2d  43338  aks5lem5a  43350  grpods  43353  unitscyglem2  43355  unitscyglem4  43357  sumcubes  43479  irrapxlem1  43938  irrapxlem2  43939  irrapxlem3  43940  pellexlem5  43949  acongrep  44096  acongeq  44099  jm2.22  44111  jm2.23  44112  jm2.26lem3  44117  jm2.27dlem2  44126  hashnzfz  45413  monoords  46421  fmul01lt1lem1  46704  fmul01lt1lem2  46705  sumnnodd  46750  limsupubuzlem  46830  dvnmul  47061  dvnprodlem1  47064  dvnprodlem2  47065  iblsplit  47084  iblspltprt  47091  itgspltprt  47097  stoweidlem3  47121  stoweidlem11  47129  stoweidlem20  47138  stoweidlem26  47144  stoweidlem34  47152  stoweidlem59  47177  stirlinglem10  47201  dirkertrigeqlem1  47216  dirkertrigeqlem2  47217  dirkertrigeqlem3  47218  dirkertrigeq  47219  dirkeritg  47220  fourierdlem11  47236  fourierdlem12  47237  fourierdlem15  47240  fourierdlem34  47259  fourierdlem41  47266  fourierdlem46  47270  fourierdlem48  47272  fourierdlem49  47273  fourierdlem50  47274  fourierdlem54  47278  fourierdlem63  47287  fourierdlem64  47288  fourierdlem65  47289  fourierdlem79  47303  fourierdlem102  47326  fourierdlem103  47327  fourierdlem104  47328  fourierdlem114  47338  elaa2lem  47351  etransclem4  47356  etransclem7  47359  etransclem8  47360  etransclem17  47369  etransclem18  47370  etransclem20  47372  etransclem23  47375  etransclem27  47379  etransclem31  47383  etransclem32  47384  etransclem35  47387  etransclem41  47393  etransclem46  47398  etransclem48  47400  iundjiun  47578  caratheodorylem1  47644  2elfz2melfz  48496  elfzelfzlble  48499  el1fzopredsuc  48504  iccpartiltu  48612  iccpartgt  48617  iccpartnel  48628  fargshiftfo  48632  altgsumbc  49572  altgsumbcALT  49573  nn0sumshdiglemA  49839  nn0sumshdiglemB  49840