Theorem elfzelz 13461

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

Syntax hints:   → wi 4   ∈ wcel 2109  ‘cfv 6499  (class class class)co 7369  ℤcz 12505  ℤ_≥cuz 12769  ...cfz 13444

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382  ax-un 7691  ax-cnex 11100  ax-resscn 11101

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 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-iun 4953  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-fv 6507  df-ov 7372  df-oprab 7373  df-mpo 7374  df-1st 7947  df-2nd 7948  df-neg 11384  df-z 12506  df-uz 12770  df-fz 13445

This theorem is referenced by:  elfzelzd  13462  fzssz  13463  elfz1eq  13472  fzsplit2  13486  fzdisj  13488  elfznn  13490  ssfzunsnext  13506  fznatpl1  13515  fzrev2i  13526  fzrev3i  13528  fznuz  13546  fzrevral  13549  fzshftral  13552  fznn0sub2  13572  elfzmlbm  13575  difelfznle  13579  predfz  13590  fzosplit  13629  sermono  13975  seqf1olem1  13982  seqf1olem2  13983  bcval2  14246  bcval4  14248  bccmpl  14250  bcp1nk  14258  bcval5  14259  bcpasc  14262  bccl2  14264  seqcoll2  14406  swrdval2  14587  swrdwrdsymb  14603  addlenrevpfx  14631  ccatpfx  14642  swrdswrd  14646  swrdpfx  14648  pfxccatin12lem2a  14668  pfxccatin12lem1  14669  swrdccatin2  14670  pfxccatin12lem2  14672  pfxccatin12  14674  spllen  14695  cshwidxm  14749  cshwidxn  14750  lswcshw  14756  2cshwcshw  14767  cshwcshid  14769  cshwcsh2id  14770  swrds2m  14883  seqshft  15027  sumrblem  15653  summolem2a  15657  fsum0diaglem  15718  mptfzshft  15720  fsumshftm  15723  fsum0diag2  15725  binomlem  15771  binom11  15774  bcxmas  15777  arisum  15802  geo2sum  15815  mertenslem1  15826  prodfn0  15836  prodrblem  15871  prodmolem2a  15876  fprodntriv  15884  fprodser  15891  fprodrev  15919  fallfacval3  15954  fallfacfwd  15978  0fallfac  15979  binomfallfaclem1  15981  binomfallfaclem2  15982  binomrisefac  15984  fallfacval4  15985  bpolycl  15994  bpolysum  15995  bpolydiflem  15996  fsumkthpow  15998  bpoly4  16001  fzm1ndvds  16268  pwp1fsum  16337  prmdvdsfz  16651  isprm7  16654  prmdvdsbc  16672  hashdvds  16721  phiprmpw  16722  prmdiveq  16732  modprminv  16746  modprminveq  16747  modprm0  16752  4sqlem11  16902  vdwapun  16921  prmop1  16985  prmdvdsprmo  16989  prmdvdsprmop  16990  prmgaplem1  16996  prmgaplem2  16997  prmgaplcmlem1  16998  prmgaplcmlem2  16999  prmgapprmo  17009  cshwshashlem1  17042  cshwshashlem2  17043  dfod2  19470  gsummptshft  19842  srgbinomlem3  20113  srgbinomlem4  20114  srgbinomlem  20115  freshmansdream  21460  chpscmatgsummon  22708  cayhamlem1  22729  iscmet3  25169  mbfi1fseqlem4  25595  itgz  25658  itgcl  25661  ibl0  25664  iblss  25682  iblss2  25683  itgss  25689  itgeqa  25691  iblconst  25695  iblabsr  25707  iblmulc2  25708  itgsplit  25713  dvfsumlem3  25911  plyeq0lem  26091  aalioulem1  26216  cxpeq  26643  birthdaylem2  26838  wilthlem1  26954  wilthlem3  26956  ftalem5  26963  basellem3  26969  basellem4  26970  dvdsppwf1o  27072  dvdsflf1o  27073  musum  27077  ppiub  27091  chtublem  27098  mersenne  27114  bposlem1  27171  lgsval2lem  27194  lgsdilem2  27220  lgsqrlem2  27234  gausslemma2dlem1a  27252  gausslemma2dlem1  27253  gausslemma2dlem3  27255  gausslemma2dlem4  27256  gausslemma2dlem5a  27257  gausslemma2dlem5  27258  gausslemma2dlem6  27259  lgseisenlem1  27262  lgseisenlem2  27263  lgseisenlem3  27264  lgsquadlem1  27267  lgsquadlem2  27268  lgsquadlem3  27269  2lgslem1a1  27276  2lgslem1a  27278  2lgslem1b  27279  rpvmasumlem  27374  dchrisumlem1  27376  dchrisumlem2  27377  dchrmusum2  27381  dchrvmasumlem1  27382  dchrvmasum2lem  27383  dchrvmasum2if  27384  dchrvmasumlem3  27386  dchrvmasumiflem1  27388  dchrvmasumiflem2  27389  dchrisum0flblem1  27395  rpvmasum2  27399  dchrisum0lem1b  27402  dchrisum0lem1  27403  dchrisum0lem2a  27404  dchrisum0lem2  27405  dchrisum0lem3  27406  dchrmusumlem  27409  dchrvmasumlem  27410  logdivbnd  27443  pntpbnd1  27473  pntlemh  27486  pntlemf  27492  ostth2lem2  27521  axlowdimlem13  28857  axlowdimlem14  28858  axlowdimlem16  28860  crctcshlem4  29723  crctcshwlkn0  29724  erclwwlkeqlen  29921  clwwnisshclwwsn  29961  eleclclwwlknlem2  29963  erclwwlkneqlen  29970  fzm1ne1  32684  fzsplit3  32689  bcm1n  32691  ballotlemfc0  34457  ballotlemfcc  34458  ballotlemodife  34462  ballotlemimin  34470  ballotlemsgt1  34475  ballotlemsel1i  34477  ballotlemsf1o  34478  ballotlemsi  34479  ballotlemsima  34480  ballotlemfg  34490  ballotlemfrc  34491  ballotlemfrcn0  34494  revpfxsfxrev  35076  swrdrevpfx  35077  pfxwlk  35084  swrdwlk  35087  erdszelem8  35158  erdszelem9  35159  cvmliftlem7  35251  supfz  35689  inffz  35690  bcprod  35698  fwddifnp1  36126  poimirlem1  37588  poimirlem14  37601  poimirlem15  37602  poimirlem16  37603  poimirlem17  37604  poimirlem19  37606  poimirlem20  37607  poimirlem23  37610  poimirlem24  37611  poimirlem27  37614  poimirlem31  37618  poimirlem32  37619  mblfinlem2  37625  iblmulc2nc  37652  fdc  37712  lcmineqlem1  41990  lcmineqlem6  41995  lcmineqlem17  42006  aks4d1p1p1  42024  aks6d1c1  42077  hashscontpow  42083  aks6d1c5lem0  42096  aks6d1c5lem3  42098  aks6d1c5  42100  sticksstones6  42112  sticksstones7  42113  sticksstones10  42116  sticksstones12a  42118  sticksstones12  42119  aks6d1c6lem1  42131  bcled  42139  bcle2d  42140  aks5lem5a  42152  grpods  42155  unitscyglem2  42157  unitscyglem4  42159  sumcubes  42274  irrapxlem1  42783  irrapxlem2  42784  irrapxlem3  42785  pellexlem5  42794  acongrep  42942  acongeq  42945  jm2.22  42957  jm2.23  42958  jm2.26lem3  42963  jm2.27dlem2  42972  hashnzfz  44282  monoords  45268  fmul01lt1lem1  45555  fmul01lt1lem2  45556  sumnnodd  45601  limsupubuzlem  45683  dvnmul  45914  dvnprodlem1  45917  dvnprodlem2  45918  iblsplit  45937  iblspltprt  45944  itgspltprt  45950  stoweidlem3  45974  stoweidlem11  45982  stoweidlem20  45991  stoweidlem26  45997  stoweidlem34  46005  stoweidlem59  46030  stirlinglem10  46054  dirkertrigeqlem1  46069  dirkertrigeqlem2  46070  dirkertrigeqlem3  46071  dirkertrigeq  46072  dirkeritg  46073  fourierdlem11  46089  fourierdlem12  46090  fourierdlem15  46093  fourierdlem34  46112  fourierdlem41  46119  fourierdlem46  46123  fourierdlem48  46125  fourierdlem49  46126  fourierdlem50  46127  fourierdlem54  46131  fourierdlem63  46140  fourierdlem64  46141  fourierdlem65  46142  fourierdlem79  46156  fourierdlem102  46179  fourierdlem103  46180  fourierdlem104  46181  fourierdlem114  46191  elaa2lem  46204  etransclem4  46209  etransclem7  46212  etransclem8  46213  etransclem17  46222  etransclem18  46223  etransclem20  46225  etransclem23  46228  etransclem27  46232  etransclem31  46236  etransclem32  46237  etransclem35  46240  etransclem41  46246  etransclem46  46251  etransclem48  46253  iundjiun  46431  caratheodorylem1  46497  2elfz2melfz  47292  elfzelfzlble  47295  el1fzopredsuc  47299  iccpartiltu  47396  iccpartgt  47401  iccpartnel  47412  fargshiftfo  47416  altgsumbc  48313  altgsumbcALT  48314  nn0sumshdiglemA  48581  nn0sumshdiglemB  48582