Theorem elfzelz 13696

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  ‘cfv 6566  (class class class)co 7451  ℤcz 12733  ℤ_≥cuz 13005  ...cfz 13679

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5255  ax-nul 5266  ax-pr 5398  ax-un 7783  ax-cnex 11295  ax-resscn 11296

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-iun 4958  df-br 5109  df-opab 5174  df-mpt 5193  df-id 5553  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-iota 6520  df-fun 6568  df-fn 6569  df-f 6570  df-fv 6574  df-ov 7454  df-oprab 7455  df-mpo 7456  df-1st 8035  df-2nd 8036  df-neg 11583  df-z 12734  df-uz 13006  df-fz 13680

This theorem is used by:  elfzelzd  13697  fzssz  13698  elfz1eq  13708  fzsplit2  13723  fzdisj  13725  elfznn  13727  ssfzunsnext  13743  fznatpl1  13752  fzrev2i  13763  fzrev3i  13765  fznuz  13783  fzrevral  13786  fzshftral  13789  fznn0sub2  13809  elfzmlbm  13812  difelfznle  13816  predfz  13827  fzosplit  13867  sermono  14217  seqf1olem1  14224  seqf1olem2  14225  bcval2  14490  bcval4  14492  bccmpl  14494  bcp1nk  14502  bcval5  14503  bcpasc  14506  bccl2  14508  seqcoll2  14651  swrdval2  14836  swrdwrdsymb  14854  ccatpfx  14892  swrdswrd  14896  swrdpfx  14898  pfxccatin12lem2a  14918  pfxccatin12lem1  14919  swrdccatin2  14920  pfxccatin12lem2  14922  pfxccatin12  14924  spllen  14945  revpfxsfxrev  14959  swrdrevpfx  14960  cshwidxm  15001  cshwidxn  15002  lswcshw  15008  2cshwcshw  15018  cshwcshid  15020  cshwcsh2id  15021  swrds2m  15135  seqshft  15281  sumrblem  15921  summolem2a  15925  fsum0diaglem  15986  mptfzshft  15988  fsumshftm  15991  fsum0diag2  15993  binomlem  16042  binom11  16045  bcxmas  16048  arisum  16073  geo2sum  16086  mertenslem1  16097  prodfn0  16107  prodrblem  16140  prodmolem2a  16145  fprodntriv  16153  fprodser  16160  fprodrev  16188  fallfacval3  16223  fallfacfwd  16246  0fallfac  16247  binomfallfaclem1  16249  binomfallfaclem2  16250  binomrisefac  16252  fallfacval4  16253  bpolycl  16262  bpolysum  16263  bpolydiflem  16264  fsumkthpow  16266  bpoly4  16269  fzm1ndvds  16536  pwp1fsum  16605  prmdvdsfz  16925  isprm7  16928  prmdvdsbc  16946  hashdvds  16996  phiprmpw  16997  prmdiveq  17007  modprminv  17021  modprminveq  17022  modprm0  17027  4sqlem11  17177  vdwapun  17196  prmop1  17260  prmdvdsprmo  17264  prmdvdsprmop  17265  prmgaplem1  17271  prmgaplem2  17272  prmgaplcmlem1  17273  prmgaplcmlem2  17274  prmgapprmo  17284  cshwshashlem1  17317  cshwshashlem2  17318  dfod2  19829  gsummptshft  20201  srgbinomlem3  20505  srgbinomlem4  20506  srgbinomlem  20507  freshmansdream  21935  chpscmatgsummon  23218  cayhamlem1  23239  iscmet3  25669  mbfi1fseqlem4  26094  itgz  26156  itgcl  26159  ibl0  26162  iblss  26180  iblss2  26181  itgss  26187  itgeqa  26189  iblconst  26193  iblabsr  26205  iblmulc2  26206  itgsplit  26211  dvfsumlem3  26403  plyeq0lem  26584  aalioulem1  26716  cxpeq  27142  birthdaylem2  27337  wilthlem1  27452  wilthlem3  27454  ftalem5  27461  basellem3  27467  basellem4  27468  dvdsppwf1o  27570  dvdsflf1o  27571  musum  27575  ppiub  27588  chtublem  27595  mersenne  27611  bposlem1  27668  lgsval2lem  27691  lgsdilem2  27717  lgsqrlem2  27731  gausslemma2dlem1a  27749  gausslemma2dlem1  27750  gausslemma2dlem3  27752  gausslemma2dlem4  27753  gausslemma2dlem5a  27754  gausslemma2dlem5  27755  gausslemma2dlem6  27756  lgseisenlem1  27759  lgseisenlem2  27760  lgseisenlem3  27761  lgsquadlem1  27764  lgsquadlem2  27765  lgsquadlem3  27766  2lgslem1a1  27773  2lgslem1a  27775  2lgslem1b  27776  rpvmasumlem  27871  dchrisumlem1  27873  dchrisumlem2  27874  dchrmusum2  27878  dchrvmasumlem1  27879  dchrvmasum2lem  27880  dchrvmasum2if  27881  dchrvmasumlem3  27883  dchrvmasumiflem1  27885  dchrvmasumiflem2  27886  dchrisum0flblem1  27892  rpvmasum2  27896  dchrisum0lem1b  27899  dchrisum0lem1  27900  dchrisum0lem2a  27901  dchrisum0lem2  27902  dchrisum0lem3  27903  dchrmusumlem  27906  dchrvmasumlem  27907  logdivbnd  27940  pntpbnd1  27970  pntlemh  27983  pntlemf  27989  ostth2lem2  28018  axlowdimlem13  29589  axlowdimlem14  29590  axlowdimlem16  29592  pfxwlk  30323  swrdwlk  30325  crctcshlem4  30466  crctcshwlkn0  30467  erclwwlkeqlen  30667  clwwnisshclwwsn  30707  eleclclwwlknlem2  30709  erclwwlkneqlen  30716  fzm1ne1  33476  fzsplit3  33481  bcm1n  33483  ballotlemfc0  35236  ballotlemfcc  35237  ballotlemodife  35241  ballotlemimin  35249  ballotlemsgt1  35254  ballotlemsel1i  35256  ballotlemsf1o  35257  ballotlemsi  35258  ballotlemsima  35259  ballotlemfg  35269  ballotlemfrc  35270  ballotlemfrcn0  35273  erdszelem8  36171  erdszelem9  36172  cvmliftlem7  36264  supfz  36709  inffz  36710  bcprod  36718  fwddifnp1  37145  poimirlem1  38807  poimirlem14  38820  poimirlem15  38821  poimirlem16  38822  poimirlem17  38823  poimirlem19  38825  poimirlem20  38826  poimirlem23  38829  poimirlem24  38830  poimirlem27  38833  poimirlem31  38837  poimirlem32  38838  mblfinlem2  38844  iblmulc2nc  38871  fdc  38945  lcmineqlem1  43345  lcmineqlem6  43350  lcmineqlem17  43361  aks4d1p1p1  43379  aks6d1c1  43432  hashscontpow  43438  aks6d1c5lem0  43451  aks6d1c5lem3  43453  aks6d1c5  43455  sticksstones6  43467  sticksstones7  43468  sticksstones10  43471  sticksstones12a  43473  sticksstones12  43474  aks6d1c6lem1  43486  bcled  43494  bcle2d  43495  aks5lem5a  43507  grpods  43510  unitscyglem2  43512  unitscyglem4  43514  sumcubes  43636  irrapxlem1  44095  irrapxlem2  44096  irrapxlem3  44097  pellexlem5  44106  acongrep  44253  acongeq  44256  jm2.22  44268  jm2.23  44269  jm2.26lem3  44274  jm2.27dlem2  44283  hashnzfz  45565  monoords  46586  fmul01lt1lem1  46869  fmul01lt1lem2  46870  sumnnodd  46915  limsupubuzlem  46995  dvnmul  47226  dvnprodlem1  47229  dvnprodlem2  47230  iblsplit  47249  iblspltprt  47256  itgspltprt  47262  stoweidlem3  47286  stoweidlem11  47294  stoweidlem20  47303  stoweidlem26  47309  stoweidlem34  47317  stoweidlem59  47342  stirlinglem10  47366  dirkertrigeqlem1  47381  dirkertrigeqlem2  47382  dirkertrigeqlem3  47383  dirkertrigeq  47384  dirkeritg  47385  fourierdlem11  47401  fourierdlem12  47402  fourierdlem15  47405  fourierdlem34  47424  fourierdlem41  47431  fourierdlem46  47435  fourierdlem48  47437  fourierdlem49  47438  fourierdlem50  47439  fourierdlem54  47443  fourierdlem63  47452  fourierdlem64  47453  fourierdlem65  47454  fourierdlem79  47468  fourierdlem102  47491  fourierdlem103  47492  fourierdlem104  47493  fourierdlem114  47503  elaa2lem  47516  etransclem4  47521  etransclem7  47524  etransclem8  47525  etransclem17  47534  etransclem18  47535  etransclem20  47537  etransclem23  47540  etransclem27  47544  etransclem31  47548  etransclem32  47549  etransclem35  47552  etransclem41  47558  etransclem46  47563  etransclem48  47565  iundjiun  47743  caratheodorylem1  47809  2elfz2melfz  48661  elfzelfzlble  48664  el1fzopredsuc  48669  iccpartiltu  48777  iccpartgt  48782  iccpartnel  48793  fargshiftfo  48797  altgsumbc  49795  altgsumbcALT  49796  nn0sumshdiglemA  50062  nn0sumshdiglemB  50063