Theorem elfzelz 13547

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

Syntax hints:   → wi 4   ∈ wcel 2143  ‘cfv 6536  (class class class)co 7410  ℤcz 12586  ℤ_≥cuz 12857  ...cfz 13530

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pr 5404  ax-un 7732  ax-cnex 11151  ax-resscn 11152

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-iun 4958  df-br 5110  df-opab 5174  df-mpt 5193  df-id 5556  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-fv 6544  df-ov 7413  df-oprab 7414  df-mpo 7415  df-1st 7982  df-2nd 7983  df-neg 11439  df-z 12587  df-uz 12858  df-fz 13531

This theorem is referenced by:  elfzelzd  13548  fzssz  13549  elfz1eq  13558  fzsplit2  13573  fzdisj  13575  elfznn  13577  ssfzunsnext  13593  fznatpl1  13602  fzrev2i  13613  fzrev3i  13615  fznuz  13633  fzrevral  13636  fzshftral  13639  fznn0sub2  13659  elfzmlbm  13662  difelfznle  13666  predfz  13677  fzosplit  13717  sermono  14066  seqf1olem1  14073  seqf1olem2  14074  bcval2  14337  bcval4  14339  bccmpl  14341  bcp1nk  14349  bcval5  14350  bcpasc  14353  bccl2  14355  seqcoll2  14498  swrdval2  14680  swrdwrdsymb  14696  ccatpfx  14734  swrdswrd  14738  swrdpfx  14740  pfxccatin12lem2a  14760  pfxccatin12lem1  14761  swrdccatin2  14762  pfxccatin12lem2  14764  pfxccatin12  14766  spllen  14787  cshwidxm  14841  cshwidxn  14842  lswcshw  14848  2cshwcshw  14858  cshwcshid  14860  cshwcsh2id  14861  swrds2m  14974  seqshft  15118  sumrblem  15758  summolem2a  15762  fsum0diaglem  15823  mptfzshft  15825  fsumshftm  15828  fsum0diag2  15830  binomlem  15879  binom11  15882  bcxmas  15885  arisum  15910  geo2sum  15923  mertenslem1  15934  prodfn0  15944  prodrblem  15979  prodmolem2a  15984  fprodntriv  15992  fprodser  15999  fprodrev  16027  fallfacval3  16062  fallfacfwd  16085  0fallfac  16086  binomfallfaclem1  16088  binomfallfaclem2  16089  binomrisefac  16091  fallfacval4  16092  bpolycl  16101  bpolysum  16102  bpolydiflem  16103  fsumkthpow  16105  bpoly4  16108  fzm1ndvds  16375  pwp1fsum  16444  prmdvdsfz  16759  isprm7  16762  prmdvdsbc  16780  hashdvds  16829  phiprmpw  16830  prmdiveq  16840  modprminv  16854  modprminveq  16855  modprm0  16860  4sqlem11  17010  vdwapun  17029  prmop1  17093  prmdvdsprmo  17097  prmdvdsprmop  17098  prmgaplem1  17104  prmgaplem2  17105  prmgaplcmlem1  17106  prmgaplcmlem2  17107  prmgapprmo  17117  cshwshashlem1  17150  cshwshashlem2  17151  dfod2  19629  gsummptshft  20001  srgbinomlem3  20305  srgbinomlem4  20306  srgbinomlem  20307  freshmansdream  21724  chpscmatgsummon  23002  cayhamlem1  23023  iscmet3  25452  mbfi1fseqlem4  25877  itgz  25940  itgcl  25943  ibl0  25946  iblss  25964  iblss2  25965  itgss  25971  itgeqa  25973  iblconst  25977  iblabsr  25989  iblmulc2  25990  itgsplit  25995  dvfsumlem3  26187  plyeq0lem  26367  aalioulem1  26495  cxpeq  26922  birthdaylem2  27117  wilthlem1  27232  wilthlem3  27234  ftalem5  27241  basellem3  27247  basellem4  27248  dvdsppwf1o  27350  dvdsflf1o  27351  musum  27355  ppiub  27368  chtublem  27375  mersenne  27391  bposlem1  27448  lgsval2lem  27471  lgsdilem2  27497  lgsqrlem2  27511  gausslemma2dlem1a  27529  gausslemma2dlem1  27530  gausslemma2dlem3  27532  gausslemma2dlem4  27533  gausslemma2dlem5a  27534  gausslemma2dlem5  27535  gausslemma2dlem6  27536  lgseisenlem1  27539  lgseisenlem2  27540  lgseisenlem3  27541  lgsquadlem1  27544  lgsquadlem2  27545  lgsquadlem3  27546  2lgslem1a1  27553  2lgslem1a  27555  2lgslem1b  27556  rpvmasumlem  27651  dchrisumlem1  27653  dchrisumlem2  27654  dchrmusum2  27658  dchrvmasumlem1  27659  dchrvmasum2lem  27660  dchrvmasum2if  27661  dchrvmasumlem3  27663  dchrvmasumiflem1  27665  dchrvmasumiflem2  27666  dchrisum0flblem1  27672  rpvmasum2  27676  dchrisum0lem1b  27679  dchrisum0lem1  27680  dchrisum0lem2a  27681  dchrisum0lem2  27682  dchrisum0lem3  27683  dchrmusumlem  27686  dchrvmasumlem  27687  logdivbnd  27720  pntpbnd1  27750  pntlemh  27763  pntlemf  27769  ostth2lem2  27798  axlowdimlem13  29304  axlowdimlem14  29305  axlowdimlem16  29307  crctcshlem4  30169  crctcshwlkn0  30170  erclwwlkeqlen  30370  clwwnisshclwwsn  30410  eleclclwwlknlem2  30412  erclwwlkneqlen  30419  fzm1ne1  33133  fzsplit3  33138  bcm1n  33140  ballotlemfc0  34883  ballotlemfcc  34884  ballotlemodife  34888  ballotlemimin  34896  ballotlemsgt1  34901  ballotlemsel1i  34903  ballotlemsf1o  34904  ballotlemsi  34905  ballotlemsima  34906  ballotlemfg  34916  ballotlemfrc  34917  ballotlemfrcn0  34920  revpfxsfxrev  35607  swrdrevpfx  35608  pfxwlk  35616  swrdwlk  35619  erdszelem8  35690  erdszelem9  35691  cvmliftlem7  35783  supfz  36221  inffz  36222  bcprod  36230  fwddifnp1  36657  poimirlem1  38272  poimirlem14  38285  poimirlem15  38286  poimirlem16  38287  poimirlem17  38288  poimirlem19  38290  poimirlem20  38291  poimirlem23  38294  poimirlem24  38295  poimirlem27  38298  poimirlem31  38302  poimirlem32  38303  mblfinlem2  38309  iblmulc2nc  38336  fdc  38396  lcmineqlem1  42796  lcmineqlem6  42801  lcmineqlem17  42812  aks4d1p1p1  42830  aks6d1c1  42883  hashscontpow  42889  aks6d1c5lem0  42902  aks6d1c5lem3  42904  aks6d1c5  42906  sticksstones6  42918  sticksstones7  42919  sticksstones10  42922  sticksstones12a  42924  sticksstones12  42925  aks6d1c6lem1  42937  bcled  42945  bcle2d  42946  aks5lem5a  42958  grpods  42961  unitscyglem2  42963  unitscyglem4  42965  sumcubes  43074  irrapxlem1  43549  irrapxlem2  43550  irrapxlem3  43551  pellexlem5  43560  acongrep  43707  acongeq  43710  jm2.22  43722  jm2.23  43723  jm2.26lem3  43728  jm2.27dlem2  43737  hashnzfz  45030  monoords  46016  fmul01lt1lem1  46300  fmul01lt1lem2  46301  sumnnodd  46346  limsupubuzlem  46426  dvnmul  46657  dvnprodlem1  46660  dvnprodlem2  46661  iblsplit  46680  iblspltprt  46687  itgspltprt  46693  stoweidlem3  46717  stoweidlem11  46725  stoweidlem20  46734  stoweidlem26  46740  stoweidlem34  46748  stoweidlem59  46773  stirlinglem10  46797  dirkertrigeqlem1  46812  dirkertrigeqlem2  46813  dirkertrigeqlem3  46814  dirkertrigeq  46815  dirkeritg  46816  fourierdlem11  46832  fourierdlem12  46833  fourierdlem15  46836  fourierdlem34  46855  fourierdlem41  46862  fourierdlem46  46866  fourierdlem48  46868  fourierdlem49  46869  fourierdlem50  46870  fourierdlem54  46874  fourierdlem63  46883  fourierdlem64  46884  fourierdlem65  46885  fourierdlem79  46899  fourierdlem102  46922  fourierdlem103  46923  fourierdlem104  46924  fourierdlem114  46934  elaa2lem  46947  etransclem4  46952  etransclem7  46955  etransclem8  46956  etransclem17  46965  etransclem18  46966  etransclem20  46968  etransclem23  46971  etransclem27  46975  etransclem31  46979  etransclem32  46980  etransclem35  46983  etransclem41  46989  etransclem46  46994  etransclem48  46996  iundjiun  47174  caratheodorylem1  47240  2elfz2melfz  48055  elfzelfzlble  48058  el1fzopredsuc  48063  iccpartiltu  48171  iccpartgt  48176  iccpartnel  48187  fargshiftfo  48191  altgsumbc  49132  altgsumbcALT  49133  nn0sumshdiglemA  49399  nn0sumshdiglemB  49400