Theorem elfzelz 10378

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

Syntax hints:   → wi 4   ∈ wcel 2205  ‘cfv 5357  (class class class)co 6058  ℤcz 9594  ℤ_≥cuz 9871  ...cfz 10361

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 619  ax-in2 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-14 2208  ax-ext 2216  ax-sep 4233  ax-pow 4292  ax-pr 4327  ax-setind 4664  ax-cnex 8234  ax-resscn 8235

This theorem depends on definitions:  df-bi 117  df-3or 1006  df-3an 1007  df-tru 1401  df-fal 1404  df-nf 1510  df-sb 1812  df-eu 2085  df-mo 2086  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ne 2415  df-ral 2527  df-rex 2528  df-rab 2531  df-v 2817  df-sbc 3046  df-dif 3216  df-un 3218  df-in 3220  df-ss 3227  df-pw 3676  df-sn 3700  df-pr 3701  df-op 3703  df-uni 3920  df-br 4115  df-opab 4177  df-mpt 4178  df-id 4419  df-xp 4760  df-rel 4761  df-cnv 4762  df-co 4763  df-dm 4764  df-rn 4765  df-res 4766  df-ima 4767  df-iota 5317  df-fun 5359  df-fn 5360  df-f 5361  df-fv 5365  df-ov 6061  df-oprab 6062  df-mpo 6063  df-neg 8463  df-z 9595  df-uz 9872  df-fz 10362

This theorem is referenced by:  elfzelzd  10379  fzssz  10380  elfz1eq  10389  fzsplit2  10404  fzdisj  10406  fzsplit3  10407  elfznn  10409  fznatpl1  10432  fzdifsuc  10437  fzrev2i  10442  fzrev3i  10444  elfzp12  10455  fznuz  10458  fzrevral  10461  fzshftral  10464  fznn0sub2  10484  elfzmlbm  10487  difelfznle  10491  fzosplit  10535  infssfzcldc  10618  infssfzledc  10619  zsupssdc  10622  ser3mono  10873  iseqf1olemkle  10883  iseqf1olemklt  10884  iseqf1olemqcl  10885  iseqf1olemnab  10887  iseqf1olemab  10888  iseqf1olemmo  10891  iseqf1olemqk  10893  seq3f1olemqsumkj  10897  seq3f1olemqsumk  10898  seq3f1olemqsum  10899  seq3f1olemstep  10900  seqf1oglem1  10905  seqf1oglem2  10906  seqfeq4g  10917  bcval2  11137  bcval4  11139  bccmpl  11141  bcp1nk  11149  bcpasc  11153  bccl2  11155  bcm1n  11156  zfz1isolemiso  11236  seq3coll  11239  swrdval2  11368  swrdlen  11369  swrdfv  11370  swrdf  11372  swrdwrdsymbg  11381  ccatswrd  11387  pfxlen  11402  ccatpfx  11418  swrdswrd  11422  pfxswrd  11423  swrdpfx  11424  lenrevpfxcctswrd  11429  pfxccatin12lem2a  11444  pfxccatin12lem1  11445  swrdccatin2  11446  pfxccatin12lem2  11448  pfxccatin12  11450  pfxccat3  11451  swrdccat3blem  11456  seq3shft  11548  sumrbdclem  12088  summodclem2a  12092  fsum0diaglem  12151  fisum0diag  12152  mptfzshft  12153  fsumrev  12154  fsumshft  12155  fsumshftm  12156  fisum0diag2  12158  binomlem  12194  binom11  12197  bcxmas  12200  arisum  12209  geo2sum  12225  cvgratnnlemabsle  12238  cvgratnnlemrate  12241  mertenslemub  12245  mertenslemi1  12246  prodfap0  12256  prodrbdclem  12282  prodmodclem2a  12287  fprodntrivap  12295  fprodm1  12309  fprod1p  12310  fprodfac  12326  fprodeq0  12328  fprodshft  12329  fprodrev  12330  fprod0diagfz  12339  fzm1ndvds  12567  lcmval  12785  lcmcllem  12789  lcmledvds  12792  prmdc  12852  prmdvdsfz  12861  isprm5lem  12863  phivalfi  12934  hashdvds  12943  phiprmpw  12944  eulerthlemrprm  12951  eulerthlema  12952  prmdiveq  12958  prmdivdiv  12959  modprminv  12972  modprminveq  12973  modprm0  12977  pcfac  13073  4sqlemafi  13118  4sqlemffi  13119  4sqleminfi  13120  4sqexercise1  13121  4sqexercise2  13122  4sqlemsdc  13123  4sqlem11  13124  4sqlem12  13125  ballotfilemcinfi  13168  ballotfilemdifcfi  13169  ballotfilemcinfz  13170  ballotfilemdifcfz  13171  ballotfilemfc0  13176  ballotfilemfcc  13177  ballotfilemefi  13181  ballotfilemodife  13184  ballotfilemscl  13191  ballotfilemsle  13192  ballotfilemimin  13193  ballotfilemsgt1  13198  ballotfilemsdom  13199  ballotfilemsel1i  13200  ballotfilemsf1o  13201  ballotfilemsi  13202  ballotfilemsima  13203  ballotfilemfg  13213  ballotfilemfrc  13214  ballotfilemfrcn0  13217  gsumshift  14105  gsumfzfsumlemm  14861  ply1termlem  15733  ply1term  15734  plyaddlem1  15738  plymullem1  15739  plymullem  15741  plycoeid3  15748  dvply1  15756  wilthlem1  15974  dvdsppwf1o  15983  mersenne  15991  lgsval2lem  16009  lgsdilem2  16035  gausslemma2dlem1a  16057  gausslemma2dlem1  16060  gausslemma2dlem3  16062  gausslemma2dlem5a  16064  gausslemma2dlem5  16065  gausslemma2dlem6  16066  lgseisenlem1  16069  lgseisenlem2  16070  lgseisenlem3  16071  lgsquadlem1  16076  lgsquadlem2  16077  lgsquadlem3  16078  2lgslem1a1  16085  2lgslem1a  16087  2lgslem1b  16088  trilpolemlt1  16951  supfz  16983  inffz  16984