Theorem elfzelz 12549

Description: A member of a finite set of sequential integer 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 12545	. 2 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ (ℤ≥‘𝑀))
2		eluzelz 11896	. 2 ⊢ (𝐾 ∈ (ℤ≥‘𝑀) → 𝐾 ∈ ℤ)
3	1, 2	syl 17	1 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2155  ‘cfv 6068  (class class class)co 6842  ℤcz 11624  ℤ_≥cuz 11886  ...cfz 12533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-sep 4941  ax-nul 4949  ax-pow 5001  ax-pr 5062  ax-un 7147  ax-cnex 10245  ax-resscn 10246

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-ral 3060  df-rex 3061  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-nul 4080  df-if 4244  df-pw 4317  df-sn 4335  df-pr 4337  df-op 4341  df-uni 4595  df-iun 4678  df-br 4810  df-opab 4872  df-mpt 4889  df-id 5185  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-fv 6076  df-ov 6845  df-oprab 6846  df-mpt2 6847  df-1st 7366  df-2nd 7367  df-neg 10523  df-z 11625  df-uz 11887  df-fz 12534

This theorem is referenced by:  fzssz  12550  elfz1eq  12559  fzsplit2  12573  fzdisj  12575  elfznn  12577  ssfzunsnext  12593  fznatpl1  12602  fzrev2i  12612  fzrev3i  12614  fznuz  12629  fzrevral  12632  fzshftral  12635  fznn0sub2  12654  elfzmlbm  12657  difelfznle  12661  predfz  12672  fzosplit  12709  fz1fzo0m1  12724  sermono  13040  seqf1olem1  13047  seqf1olem2  13048  bcval2  13296  bcval4  13298  bccmpl  13300  bcp1nk  13308  bcval5  13309  bcpasc  13312  bccl2  13314  seqcoll  13449  seqcoll2  13450  swrdval2  13621  swrd0valOLD  13622  addlenrevswrdOLD  13639  swrd0fvOLD  13641  ccatswrd  13658  addlenrevpfx  13677  ccatpfx  13688  swrdswrd  13692  swrdswrd0OLD  13695  swrdpfx  13696  swrdccatin12lem2a  13731  pfxccatin12lem1  13732  swrdccatin12lem2bOLD  13733  swrdccatin2  13734  pfxccatin12lem2  13736  pfxccatin12  13739  swrdccatin12OLD  13740  spllen  13774  spllenOLD  13775  splfv1  13776  splfv1OLD  13777  cshwidxm  13837  cshwidxn  13838  lswcshw  13844  2cshwcshw  13854  cshwcshid  13856  cshwcsh2id  13857  swrds2m  13970  seqshft  14110  sumrblem  14727  summolem2a  14731  fsum0diaglem  14792  mptfzshft  14794  fsumrev  14795  fsumshftm  14797  fsum0diag2  14799  binomlem  14845  binom11  14848  bcxmas  14851  arisum  14876  geo2sum  14888  mertenslem1  14899  prodfn0  14909  prodrblem  14942  prodmolem2a  14947  fprodntriv  14955  fprodser  14962  fprod1p  14981  fprodrev  14990  fallfacval3  15025  fallfacfwd  15049  0fallfac  15050  binomfallfaclem1  15052  binomfallfaclem2  15053  binomrisefac  15055  fallfacval4  15056  bpolycl  15065  bpolysum  15066  bpolydiflem  15067  fsumkthpow  15069  bpoly4  15072  fzm1ndvds  15329  pwp1fsum  15396  prmdvdsfz  15696  isprm7  15699  hashdvds  15759  phiprmpw  15760  prmdiveq  15770  prmdivdiv  15771  modprminv  15783  modprminveq  15784  modprm0  15789  4sqlem11  15938  4sqlem12  15939  vdwapun  15957  prmop1  16021  prmdvdsprmo  16025  prmdvdsprmop  16026  prmgaplem1  16032  prmgaplem2  16033  prmgaplcmlem1  16034  prmgaplcmlem2  16035  prmgapprmo  16045  cshwshashlem1  16076  cshwshashlem2  16077  dfod2  18245  efgredleme  18421  efgredlemc  18423  efgredlemb  18424  gsummptshft  18602  srgbinomlem3  18809  srgbinomlem4  18810  srgbinomlem  18811  chpscmatgsummon  20929  cayhamlem1  20950  iscmet3  23370  mbfi1fseqlem4  23776  itgz  23838  itgcl  23841  ibl0  23844  iblss  23862  iblss2  23863  itgss  23869  itgeqa  23871  iblconst  23875  iblabsr  23887  iblmulc2  23888  itgsplit  23893  dvfsumlem3  24082  plyeq0lem  24257  aalioulem1  24378  cxpeq  24789  birthdaylem2  24970  wilthlem1  25085  wilthlem2  25086  wilthlem3  25087  ftalem5  25094  basellem3  25100  basellem4  25101  dvdsppwf1o  25203  dvdsflf1o  25204  musum  25208  ppiub  25220  chtublem  25227  mersenne  25243  bposlem1  25300  lgsval2lem  25323  lgsdilem2  25349  lgsqrlem2  25363  lgsqrlem4  25365  gausslemma2dlem1a  25381  gausslemma2dlem1  25382  gausslemma2dlem3  25384  gausslemma2dlem4  25385  gausslemma2dlem5a  25386  gausslemma2dlem5  25387  gausslemma2dlem6  25388  lgseisenlem1  25391  lgseisenlem2  25392  lgseisenlem3  25393  lgsquadlem1  25396  lgsquadlem2  25397  lgsquadlem3  25398  2lgslem1a1  25405  2lgslem1a  25407  2lgslem1b  25408  rpvmasumlem  25467  dchrisumlem1  25469  dchrisumlem2  25470  dchrmusum2  25474  dchrvmasumlem1  25475  dchrvmasum2lem  25476  dchrvmasum2if  25477  dchrvmasumlem3  25479  dchrvmasumiflem1  25481  dchrvmasumiflem2  25482  dchrisum0flblem1  25488  rpvmasum2  25492  dchrisum0lem1b  25495  dchrisum0lem1  25496  dchrisum0lem2a  25497  dchrisum0lem2  25498  dchrisum0lem3  25499  dchrmusumlem  25502  dchrvmasumlem  25503  logdivbnd  25536  pntpbnd1  25566  pntlemh  25579  pntlemj  25583  pntlemf  25585  ostth2lem2  25614  axlowdimlem13  26125  axlowdimlem14  26126  axlowdimlem16  26128  crctcshlem4  27005  crctcshwlkn0  27006  erclwwlkeqlen  27255  clwwnisshclwwsn  27311  eleclclwwlknlem2  27313  erclwwlkneqlen  27320  clwlksfclwwlkOLD  27337  fzsplit3  30002  bcm1n  30003  ballotlemfc0  31002  ballotlemfcc  31003  ballotlemodife  31007  ballotlemimin  31015  ballotlemsgt1  31020  ballotlemsel1i  31022  ballotlemsf1o  31023  ballotlemsi  31024  ballotlemsima  31025  ballotlemfg  31035  ballotlemfrc  31036  ballotlemfrceq  31038  ballotlemfrcn0  31039  ballotlemirc  31041  ballotlem1ri  31044  erdszelem8  31628  erdszelem9  31629  cvmliftlem7  31721  supfz  32059  inffz  32060  bcprod  32069  fwddifnp1  32716  poimirlem1  33834  poimirlem2  33835  poimirlem7  33840  poimirlem14  33847  poimirlem15  33848  poimirlem16  33849  poimirlem17  33850  poimirlem19  33852  poimirlem20  33853  poimirlem23  33856  poimirlem24  33857  poimirlem27  33860  poimirlem28  33861  poimirlem31  33864  poimirlem32  33865  mblfinlem2  33871  iblmulc2nc  33898  fdc  33963  irrapxlem1  38064  irrapxlem2  38065  irrapxlem3  38066  pellexlem5  38075  acongrep  38224  fzmaxdif  38225  acongeq  38227  jm2.22  38239  jm2.23  38240  jm2.26lem3  38245  jm2.26  38246  jm2.27dlem2  38254  hashnzfz  39193  monoords  40150  elfzelzd  40168  fmul01lt1lem1  40454  fmul01lt1lem2  40455  sumnnodd  40500  limsupubuzlem  40582  dvnmul  40796  dvnprodlem2  40800  iblsplit  40819  iblspltprt  40826  itgspltprt  40832  stoweidlem3  40857  stoweidlem11  40865  stoweidlem20  40874  stoweidlem26  40880  stoweidlem34  40888  stoweidlem59  40913  stirlinglem10  40937  dirkertrigeqlem1  40952  dirkertrigeqlem2  40953  dirkertrigeqlem3  40954  dirkertrigeq  40955  dirkeritg  40956  fourierdlem11  40972  fourierdlem12  40973  fourierdlem15  40976  fourierdlem34  40995  fourierdlem41  41002  fourierdlem46  41006  fourierdlem48  41008  fourierdlem49  41009  fourierdlem50  41010  fourierdlem54  41014  fourierdlem63  41023  fourierdlem64  41024  fourierdlem65  41025  fourierdlem79  41039  fourierdlem102  41062  fourierdlem103  41063  fourierdlem104  41064  fourierdlem114  41074  elaa2lem  41087  etransclem4  41092  etransclem7  41095  etransclem8  41096  etransclem17  41105  etransclem18  41106  etransclem20  41108  etransclem23  41111  etransclem27  41115  etransclem31  41119  etransclem32  41120  etransclem35  41123  etransclem41  41129  etransclem46  41134  etransclem48  41136  iundjiun  41314  caratheodorylem1  41380  2elfz2melfz  42062  elfzelfzlble  42065  el1fzopredsuc  42069  iccpartgtprec  42090  iccpartiltu  42092  iccpartgt  42097  iccpartnel  42108  fargshiftfo  42112  altgsumbc  42799  altgsumbcALT  42800  nn0sumshdiglemA  43082  nn0sumshdiglemB  43083