Theorem elfzelz 13539

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 13535	. 2 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ (ℤ≥‘𝑀))
2		eluzelz 12860	. 2 ⊢ (𝐾 ∈ (ℤ≥‘𝑀) → 𝐾 ∈ ℤ)
3	1, 2	syl 17	1 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2108  ‘cfv 6530  (class class class)co 7403  ℤcz 12586  ℤ_≥cuz 12850  ...cfz 13522

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402  ax-un 7727  ax-cnex 11183  ax-resscn 11184

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-iun 4969  df-br 5120  df-opab 5182  df-mpt 5202  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-iota 6483  df-fun 6532  df-fn 6533  df-f 6534  df-fv 6538  df-ov 7406  df-oprab 7407  df-mpo 7408  df-1st 7986  df-2nd 7987  df-neg 11467  df-z 12587  df-uz 12851  df-fz 13523

This theorem is referenced by:  elfzelzd  13540  fzssz  13541  elfz1eq  13550  fzsplit2  13564  fzdisj  13566  elfznn  13568  ssfzunsnext  13584  fznatpl1  13593  fzrev2i  13604  fzrev3i  13606  fznuz  13624  fzrevral  13627  fzshftral  13630  fznn0sub2  13650  elfzmlbm  13653  difelfznle  13657  predfz  13668  fzosplit  13707  sermono  14050  seqf1olem1  14057  seqf1olem2  14058  bcval2  14321  bcval4  14323  bccmpl  14325  bcp1nk  14333  bcval5  14334  bcpasc  14337  bccl2  14339  seqcoll2  14481  swrdval2  14662  swrdwrdsymb  14678  addlenrevpfx  14706  ccatpfx  14717  swrdswrd  14721  swrdpfx  14723  pfxccatin12lem2a  14743  pfxccatin12lem1  14744  swrdccatin2  14745  pfxccatin12lem2  14747  pfxccatin12  14749  spllen  14770  cshwidxm  14824  cshwidxn  14825  lswcshw  14831  2cshwcshw  14842  cshwcshid  14844  cshwcsh2id  14845  swrds2m  14958  seqshft  15102  sumrblem  15725  summolem2a  15729  fsum0diaglem  15790  mptfzshft  15792  fsumshftm  15795  fsum0diag2  15797  binomlem  15843  binom11  15846  bcxmas  15849  arisum  15874  geo2sum  15887  mertenslem1  15898  prodfn0  15908  prodrblem  15943  prodmolem2a  15948  fprodntriv  15956  fprodser  15963  fprodrev  15991  fallfacval3  16026  fallfacfwd  16050  0fallfac  16051  binomfallfaclem1  16053  binomfallfaclem2  16054  binomrisefac  16056  fallfacval4  16057  bpolycl  16066  bpolysum  16067  bpolydiflem  16068  fsumkthpow  16070  bpoly4  16073  fzm1ndvds  16339  pwp1fsum  16408  prmdvdsfz  16722  isprm7  16725  prmdvdsbc  16743  hashdvds  16792  phiprmpw  16793  prmdiveq  16803  modprminv  16817  modprminveq  16818  modprm0  16823  4sqlem11  16973  vdwapun  16992  prmop1  17056  prmdvdsprmo  17060  prmdvdsprmop  17061  prmgaplem1  17067  prmgaplem2  17068  prmgaplcmlem1  17069  prmgaplcmlem2  17070  prmgapprmo  17080  cshwshashlem1  17113  cshwshashlem2  17114  dfod2  19543  gsummptshft  19915  srgbinomlem3  20186  srgbinomlem4  20187  srgbinomlem  20188  freshmansdream  21533  chpscmatgsummon  22781  cayhamlem1  22802  iscmet3  25243  mbfi1fseqlem4  25669  itgz  25732  itgcl  25735  ibl0  25738  iblss  25756  iblss2  25757  itgss  25763  itgeqa  25765  iblconst  25769  iblabsr  25781  iblmulc2  25782  itgsplit  25787  dvfsumlem3  25985  plyeq0lem  26165  aalioulem1  26290  cxpeq  26717  birthdaylem2  26912  wilthlem1  27028  wilthlem3  27030  ftalem5  27037  basellem3  27043  basellem4  27044  dvdsppwf1o  27146  dvdsflf1o  27147  musum  27151  ppiub  27165  chtublem  27172  mersenne  27188  bposlem1  27245  lgsval2lem  27268  lgsdilem2  27294  lgsqrlem2  27308  gausslemma2dlem1a  27326  gausslemma2dlem1  27327  gausslemma2dlem3  27329  gausslemma2dlem4  27330  gausslemma2dlem5a  27331  gausslemma2dlem5  27332  gausslemma2dlem6  27333  lgseisenlem1  27336  lgseisenlem2  27337  lgseisenlem3  27338  lgsquadlem1  27341  lgsquadlem2  27342  lgsquadlem3  27343  2lgslem1a1  27350  2lgslem1a  27352  2lgslem1b  27353  rpvmasumlem  27448  dchrisumlem1  27450  dchrisumlem2  27451  dchrmusum2  27455  dchrvmasumlem1  27456  dchrvmasum2lem  27457  dchrvmasum2if  27458  dchrvmasumlem3  27460  dchrvmasumiflem1  27462  dchrvmasumiflem2  27463  dchrisum0flblem1  27469  rpvmasum2  27473  dchrisum0lem1b  27476  dchrisum0lem1  27477  dchrisum0lem2a  27478  dchrisum0lem2  27479  dchrisum0lem3  27480  dchrmusumlem  27483  dchrvmasumlem  27484  logdivbnd  27517  pntpbnd1  27547  pntlemh  27560  pntlemf  27566  ostth2lem2  27595  axlowdimlem13  28879  axlowdimlem14  28880  axlowdimlem16  28882  crctcshlem4  29748  crctcshwlkn0  29749  erclwwlkeqlen  29946  clwwnisshclwwsn  29986  eleclclwwlknlem2  29988  erclwwlkneqlen  29995  fzm1ne1  32711  fzsplit3  32716  bcm1n  32718  ballotlemfc0  34471  ballotlemfcc  34472  ballotlemodife  34476  ballotlemimin  34484  ballotlemsgt1  34489  ballotlemsel1i  34491  ballotlemsf1o  34492  ballotlemsi  34493  ballotlemsima  34494  ballotlemfg  34504  ballotlemfrc  34505  ballotlemfrcn0  34508  revpfxsfxrev  35084  swrdrevpfx  35085  pfxwlk  35092  swrdwlk  35095  erdszelem8  35166  erdszelem9  35167  cvmliftlem7  35259  supfz  35692  inffz  35693  bcprod  35701  fwddifnp1  36129  poimirlem1  37591  poimirlem14  37604  poimirlem15  37605  poimirlem16  37606  poimirlem17  37607  poimirlem19  37609  poimirlem20  37610  poimirlem23  37613  poimirlem24  37614  poimirlem27  37617  poimirlem31  37621  poimirlem32  37622  mblfinlem2  37628  iblmulc2nc  37655  fdc  37715  lcmineqlem1  41988  lcmineqlem6  41993  lcmineqlem17  42004  aks4d1p1p1  42022  aks6d1c1  42075  hashscontpow  42081  aks6d1c5lem0  42094  aks6d1c5lem3  42096  aks6d1c5  42098  sticksstones6  42110  sticksstones7  42111  sticksstones10  42114  sticksstones12a  42116  sticksstones12  42117  aks6d1c6lem1  42129  bcled  42137  bcle2d  42138  aks5lem5a  42150  grpods  42153  unitscyglem2  42155  unitscyglem4  42157  metakunt15  42178  metakunt16  42179  metakunt19  42182  metakunt25  42188  metakunt33  42196  sumcubes  42309  irrapxlem1  42792  irrapxlem2  42793  irrapxlem3  42794  pellexlem5  42803  acongrep  42951  acongeq  42954  jm2.22  42966  jm2.23  42967  jm2.26lem3  42972  jm2.27dlem2  42981  hashnzfz  44292  monoords  45274  fmul01lt1lem1  45561  fmul01lt1lem2  45562  sumnnodd  45607  limsupubuzlem  45689  dvnmul  45920  dvnprodlem1  45923  dvnprodlem2  45924  iblsplit  45943  iblspltprt  45950  itgspltprt  45956  stoweidlem3  45980  stoweidlem11  45988  stoweidlem20  45997  stoweidlem26  46003  stoweidlem34  46011  stoweidlem59  46036  stirlinglem10  46060  dirkertrigeqlem1  46075  dirkertrigeqlem2  46076  dirkertrigeqlem3  46077  dirkertrigeq  46078  dirkeritg  46079  fourierdlem11  46095  fourierdlem12  46096  fourierdlem15  46099  fourierdlem34  46118  fourierdlem41  46125  fourierdlem46  46129  fourierdlem48  46131  fourierdlem49  46132  fourierdlem50  46133  fourierdlem54  46137  fourierdlem63  46146  fourierdlem64  46147  fourierdlem65  46148  fourierdlem79  46162  fourierdlem102  46185  fourierdlem103  46186  fourierdlem104  46187  fourierdlem114  46197  elaa2lem  46210  etransclem4  46215  etransclem7  46218  etransclem8  46219  etransclem17  46228  etransclem18  46229  etransclem20  46231  etransclem23  46234  etransclem27  46238  etransclem31  46242  etransclem32  46243  etransclem35  46246  etransclem41  46252  etransclem46  46257  etransclem48  46259  iundjiun  46437  caratheodorylem1  46503  2elfz2melfz  47295  elfzelfzlble  47298  el1fzopredsuc  47302  iccpartiltu  47384  iccpartgt  47389  iccpartnel  47400  fargshiftfo  47404  altgsumbc  48275  altgsumbcALT  48276  nn0sumshdiglemA  48547  nn0sumshdiglemB  48548