Theorem eluzfz1 13587

Description: Membership in a finite set of sequential integers - special case. (Contributed by NM, 21-Jul-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)

Assertion

Ref	Expression
eluzfz1	⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ (𝑀...𝑁))

Proof of Theorem eluzfz1

Step	Hyp	Ref	Expression
1		eluzel2 12895	. . 3 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ)
2		uzid 12905	. . 3 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ≥‘𝑀))
3	1, 2	syl 18	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ (ℤ≥‘𝑀))
4		eluzfz 13575	. 2 ⊢ ((𝑀 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝑀)) → 𝑀 ∈ (𝑀...𝑁))
5	3, 4	mpancom 701	1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ (𝑀...𝑁))

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ‘cfv 6537  (class class class)co 7416  ℤcz 12618  ℤ_≥cuz 12890  ...cfz 13563

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402  ax-un 7739  ax-cnex 11183  ax-resscn 11184  ax-pre-lttri 11201

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 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3064  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-iun 4956  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-ov 7419  df-oprab 7420  df-mpo 7421  df-1st 7989  df-2nd 7990  df-er 8699  df-en 8956  df-dom 8957  df-sdom 8958  df-pnf 11272  df-mnf 11273  df-xr 11274  df-ltxr 11275  df-le 11276  df-neg 11471  df-z 12619  df-uz 12891  df-fz 13564

This theorem is used by:  elfz3  13590  fzn0  13594  fzopth  13618  seqcl  14088  seqfveq  14092  seqshft2  14094  monoord  14098  monoord2  14099  seqcaopr3  14103  seqf1olem2a  14106  seqf1olem2  14108  seqhomo  14115  seqcoll  14531  fsum1p  15841  telfsumo  15891  telfsumo2  15892  fsumparts  15895  mertenslem2  15976  prodfn0  15985  prodfrec  15986  fprod1p  16059  phicl2  16863  eulerthlem2  16877  4sqlem19  17059  vdwlem1  17077  vdwlem6  17082  vdw  17090  fvprmselelfz  17140  prmodvdslcmf  17143  gsumval2  18790  gsumsplit1r  18791  efgsdmi  19860  gsumval3  20035  telgsumfzslem  20116  telgsumfzs  20117  pmatcollpw3fi1lem1  23012  chfacfisf  23080  chfacfisfcpmat  23081  cpmadugsumlemF  23102  imasdsf1olem  24600  ovoliunlem1  25731  mbfi1fseqlem3  25946  cxpeq  26992  ppiltx  27411  logexprlim  27459  dchrmusum2  27728  dchrvmasum2lem  27730  mudivsum  27764  mulogsum  27766  mulog2sumlem2  27769  axlowdimlem13  29397  axlowdim1  29402  axlowdim  29404  crctcshwlkn0lem6  30269  gsummptfzsplitla  33486  fzto1stfv1  33528  fzto1stinvn  33531  cycpmco2f1  33551  lmatfval  34311  lmat22e11  34315  ballotlem4  34997  ballotlemic  35005  ballotlem1c  35006  ballotlem1ri  35033  subfacp1lem1  35745  subfacp1lem5  35750  subfacp1lem6  35751  cvmliftlem10  35860  cvmliftlem13  35862  inffz  36296  fwddifnp1  36732  poimirlem6  38362  poimirlem7  38363  poimirlem16  38372  poimirlem17  38373  poimirlem19  38375  poimirlem28  38384  fdc  38482  mettrifi  38494  sticksstones12a  43010  monoordxrv  46296  monoord2xrv  46298  fmul01lt1lem1  46401  dvnmptdivc  46753  dvnmul  46758  itgspltprt  46794  stoweidlem17  46832  stoweidlem20  46835  stoweidlem34  46849  fourierdlem15  46937  fourierdlem48  46969  fourierdlem50  46971  fourierdlem52  46973  fourierdlem54  46975  fourierdlem64  46985  fourierdlem81  47002  fourierdlem102  47023  fourierdlem103  47024  fourierdlem104  47025  fourierdlem111  47032  fourierdlem114  47035  etransclem10  47059  etransclem14  47063  etransclem15  47064  etransclem24  47073  etransclem35  47084  etransclem44  47093  smfmullem4  47609  ssfz12  48189  smonoord  48252  gpg5grlim  48996  gpg5grlic  48997