Theorem elfzelz 13265

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

Syntax hints:   → wi 4   ∈ wcel 2107  ‘cfv 6437  (class class class)co 7284  ℤcz 12328  ℤ_≥cuz 12591  ...cfz 13248

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-sep 5224  ax-nul 5231  ax-pr 5353  ax-un 7597  ax-cnex 10936  ax-resscn 10937

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3435  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-pw 4536  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-iun 4927  df-br 5076  df-opab 5138  df-mpt 5159  df-id 5490  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-iota 6395  df-fun 6439  df-fn 6440  df-f 6441  df-fv 6445  df-ov 7287  df-oprab 7288  df-mpo 7289  df-1st 7840  df-2nd 7841  df-neg 11217  df-z 12329  df-uz 12592  df-fz 13249

This theorem is referenced by:  elfzelzd  13266  fzssz  13267  elfz1eq  13276  fzsplit2  13290  fzdisj  13292  elfznn  13294  ssfzunsnext  13310  fznatpl1  13319  fzrev2i  13330  fzrev3i  13332  fznuz  13347  fzrevral  13350  fzshftral  13353  fznn0sub2  13372  elfzmlbm  13375  difelfznle  13379  predfz  13390  fzosplit  13429  sermono  13764  seqf1olem1  13771  seqf1olem2  13772  bcval2  14028  bcval4  14030  bccmpl  14032  bcp1nk  14040  bcval5  14041  bcpasc  14044  bccl2  14046  seqcoll2  14188  swrdval2  14368  swrdwrdsymb  14384  addlenrevpfx  14412  ccatpfx  14423  swrdswrd  14427  swrdpfx  14429  pfxccatin12lem2a  14449  pfxccatin12lem1  14450  swrdccatin2  14451  pfxccatin12lem2  14453  pfxccatin12  14455  spllen  14476  cshwidxm  14530  cshwidxn  14531  lswcshw  14537  2cshwcshw  14547  cshwcshid  14549  cshwcsh2id  14550  swrds2m  14663  seqshft  14805  sumrblem  15432  summolem2a  15436  fsum0diaglem  15497  mptfzshft  15499  fsumshftm  15502  fsum0diag2  15504  binomlem  15550  binom11  15553  bcxmas  15556  arisum  15581  geo2sum  15594  mertenslem1  15605  prodfn0  15615  prodrblem  15648  prodmolem2a  15653  fprodntriv  15661  fprodser  15668  fprodrev  15696  fallfacval3  15731  fallfacfwd  15755  0fallfac  15756  binomfallfaclem1  15758  binomfallfaclem2  15759  binomrisefac  15761  fallfacval4  15762  bpolycl  15771  bpolysum  15772  bpolydiflem  15773  fsumkthpow  15775  bpoly4  15778  fzm1ndvds  16040  pwp1fsum  16109  prmdvdsfz  16419  isprm7  16422  hashdvds  16485  phiprmpw  16486  prmdiveq  16496  modprminv  16509  modprminveq  16510  modprm0  16515  4sqlem11  16665  vdwapun  16684  prmop1  16748  prmdvdsprmo  16752  prmdvdsprmop  16753  prmgaplem1  16759  prmgaplem2  16760  prmgaplcmlem1  16761  prmgaplcmlem2  16762  prmgapprmo  16772  cshwshashlem1  16806  cshwshashlem2  16807  dfod2  19180  gsummptshft  19546  srgbinomlem3  19787  srgbinomlem4  19788  srgbinomlem  19789  chpscmatgsummon  22003  cayhamlem1  22024  iscmet3  24466  mbfi1fseqlem4  24892  itgz  24954  itgcl  24957  ibl0  24960  iblss  24978  iblss2  24979  itgss  24985  itgeqa  24987  iblconst  24991  iblabsr  25003  iblmulc2  25004  itgsplit  25009  dvfsumlem3  25201  plyeq0lem  25380  aalioulem1  25501  cxpeq  25919  birthdaylem2  26111  wilthlem1  26226  wilthlem3  26228  ftalem5  26235  basellem3  26241  basellem4  26242  dvdsppwf1o  26344  dvdsflf1o  26345  musum  26349  ppiub  26361  chtublem  26368  mersenne  26384  bposlem1  26441  lgsval2lem  26464  lgsdilem2  26490  lgsqrlem2  26504  gausslemma2dlem1a  26522  gausslemma2dlem1  26523  gausslemma2dlem3  26525  gausslemma2dlem4  26526  gausslemma2dlem5a  26527  gausslemma2dlem5  26528  gausslemma2dlem6  26529  lgseisenlem1  26532  lgseisenlem2  26533  lgseisenlem3  26534  lgsquadlem1  26537  lgsquadlem2  26538  lgsquadlem3  26539  2lgslem1a1  26546  2lgslem1a  26548  2lgslem1b  26549  rpvmasumlem  26644  dchrisumlem1  26646  dchrisumlem2  26647  dchrmusum2  26651  dchrvmasumlem1  26652  dchrvmasum2lem  26653  dchrvmasum2if  26654  dchrvmasumlem3  26656  dchrvmasumiflem1  26658  dchrvmasumiflem2  26659  dchrisum0flblem1  26665  rpvmasum2  26669  dchrisum0lem1b  26672  dchrisum0lem1  26673  dchrisum0lem2a  26674  dchrisum0lem2  26675  dchrisum0lem3  26676  dchrmusumlem  26679  dchrvmasumlem  26680  logdivbnd  26713  pntpbnd1  26743  pntlemh  26756  pntlemf  26762  ostth2lem2  26791  axlowdimlem13  27331  axlowdimlem14  27332  axlowdimlem16  27334  crctcshlem4  28194  crctcshwlkn0  28195  erclwwlkeqlen  28392  clwwnisshclwwsn  28432  eleclclwwlknlem2  28434  erclwwlkneqlen  28441  fzm1ne1  31119  fzsplit3  31124  bcm1n  31125  prmdvdsbc  31139  freshmansdream  31493  ballotlemfc0  32468  ballotlemfcc  32469  ballotlemodife  32473  ballotlemimin  32481  ballotlemsgt1  32486  ballotlemsel1i  32488  ballotlemsf1o  32489  ballotlemsi  32490  ballotlemsima  32491  ballotlemfg  32501  ballotlemfrc  32502  ballotlemfrcn0  32505  revpfxsfxrev  33086  swrdrevpfx  33087  pfxwlk  33094  swrdwlk  33097  erdszelem8  33169  erdszelem9  33170  cvmliftlem7  33262  supfz  33703  inffz  33704  bcprod  33713  fwddifnp1  34476  poimirlem1  35787  poimirlem14  35800  poimirlem15  35801  poimirlem16  35802  poimirlem17  35803  poimirlem19  35805  poimirlem20  35806  poimirlem23  35809  poimirlem24  35810  poimirlem27  35813  poimirlem31  35817  poimirlem32  35818  mblfinlem2  35824  iblmulc2nc  35851  fdc  35912  lcmineqlem1  40044  lcmineqlem6  40049  lcmineqlem17  40060  aks4d1p1p1  40078  sticksstones6  40114  sticksstones7  40115  sticksstones10  40118  sticksstones12a  40120  sticksstones12  40121  metakunt15  40146  metakunt16  40147  metakunt19  40150  metakunt25  40156  metakunt33  40164  irrapxlem1  40651  irrapxlem2  40652  irrapxlem3  40653  pellexlem5  40662  acongrep  40809  acongeq  40812  jm2.22  40824  jm2.23  40825  jm2.26lem3  40830  jm2.27dlem2  40839  hashnzfz  41945  monoords  42843  fmul01lt1lem1  43132  fmul01lt1lem2  43133  sumnnodd  43178  limsupubuzlem  43260  dvnmul  43491  dvnprodlem2  43495  iblsplit  43514  iblspltprt  43521  itgspltprt  43527  stoweidlem3  43551  stoweidlem11  43559  stoweidlem20  43568  stoweidlem26  43574  stoweidlem34  43582  stoweidlem59  43607  stirlinglem10  43631  dirkertrigeqlem1  43646  dirkertrigeqlem2  43647  dirkertrigeqlem3  43648  dirkertrigeq  43649  dirkeritg  43650  fourierdlem11  43666  fourierdlem12  43667  fourierdlem15  43670  fourierdlem34  43689  fourierdlem41  43696  fourierdlem46  43700  fourierdlem48  43702  fourierdlem49  43703  fourierdlem50  43704  fourierdlem54  43708  fourierdlem63  43717  fourierdlem64  43718  fourierdlem65  43719  fourierdlem79  43733  fourierdlem102  43756  fourierdlem103  43757  fourierdlem104  43758  fourierdlem114  43768  elaa2lem  43781  etransclem4  43786  etransclem7  43789  etransclem8  43790  etransclem17  43799  etransclem18  43800  etransclem20  43802  etransclem23  43805  etransclem27  43809  etransclem31  43813  etransclem32  43814  etransclem35  43817  etransclem41  43823  etransclem46  43828  etransclem48  43830  iundjiun  44005  caratheodorylem1  44071  2elfz2melfz  44821  elfzelfzlble  44824  el1fzopredsuc  44828  iccpartiltu  44885  iccpartgt  44890  iccpartnel  44901  fargshiftfo  44905  altgsumbc  45699  altgsumbcALT  45700  nn0sumshdiglemA  45976  nn0sumshdiglemB  45977