Theorem eluzfz1 13449

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 12758	. . 3 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ)
2		uzid 12768	. . 3 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ≥‘𝑀))
3	1, 2	syl 17	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ (ℤ≥‘𝑀))
4		eluzfz 13437	. 2 ⊢ ((𝑀 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝑀)) → 𝑀 ∈ (𝑀...𝑁))
5	3, 4	mpancom 689	1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ (𝑀...𝑁))

Syntax hints:   → wi 4   ∈ wcel 2114  ‘cfv 6491  (class class class)co 7358  ℤcz 12490  ℤ_≥cuz 12753  ...cfz 13425

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2183  ax-ext 2707  ax-sep 5240  ax-nul 5250  ax-pow 5309  ax-pr 5376  ax-un 7680  ax-cnex 11084  ax-resscn 11085  ax-pre-lttri 11102

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2538  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2810  df-nfc 2884  df-ne 2932  df-nel 3036  df-ral 3051  df-rex 3060  df-rab 3399  df-v 3441  df-sbc 3740  df-csb 3849  df-dif 3903  df-un 3905  df-in 3907  df-ss 3917  df-nul 4285  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-iun 4947  df-br 5098  df-opab 5160  df-mpt 5179  df-id 5518  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-iota 6447  df-fun 6493  df-fn 6494  df-f 6495  df-f1 6496  df-fo 6497  df-f1o 6498  df-fv 6499  df-ov 7361  df-oprab 7362  df-mpo 7363  df-1st 7933  df-2nd 7934  df-er 8635  df-en 8886  df-dom 8887  df-sdom 8888  df-pnf 11170  df-mnf 11171  df-xr 11172  df-ltxr 11173  df-le 11174  df-neg 11369  df-z 12491  df-uz 12754  df-fz 13426

This theorem is referenced by:  elfz3  13452  fzn0  13456  fzopth  13479  seqcl  13947  seqfveq  13951  seqshft2  13953  monoord  13957  monoord2  13958  seqcaopr3  13962  seqf1olem2a  13965  seqf1olem2  13967  seqhomo  13974  seqcoll  14389  fsum1p  15678  telfsumo  15727  telfsumo2  15728  fsumparts  15731  mertenslem2  15810  prodfn0  15819  prodfrec  15820  fprod1p  15893  phicl2  16697  eulerthlem2  16711  4sqlem19  16893  vdwlem1  16911  vdwlem6  16916  vdw  16924  fvprmselelfz  16974  prmodvdslcmf  16977  gsumval2  18613  gsumsplit1r  18614  efgsdmi  19663  gsumval3  19838  telgsumfzslem  19919  telgsumfzs  19920  pmatcollpw3fi1lem1  22732  chfacfisf  22800  chfacfisfcpmat  22801  cpmadugsumlemF  22822  imasdsf1olem  24319  ovoliunlem1  25461  mbfi1fseqlem3  25676  cxpeq  26725  ppiltx  27145  logexprlim  27194  dchrmusum2  27463  dchrvmasum2lem  27465  mudivsum  27499  mulogsum  27501  mulog2sumlem2  27504  axlowdimlem13  29008  axlowdim1  29013  axlowdim  29015  crctcshwlkn0lem6  29869  gsummptfzsplitla  33121  fzto1stfv1  33162  fzto1stinvn  33165  cycpmco2f1  33185  lmatfval  33950  lmat22e11  33954  ballotlem4  34635  ballotlemic  34643  ballotlem1c  34644  ballotlem1ri  34671  subfacp1lem1  35352  subfacp1lem5  35357  subfacp1lem6  35358  cvmliftlem10  35467  cvmliftlem13  35469  inffz  35903  fwddifnp1  36338  poimirlem6  37796  poimirlem7  37797  poimirlem16  37806  poimirlem17  37807  poimirlem19  37809  poimirlem28  37818  fdc  37915  mettrifi  37927  sticksstones12a  42446  monoordxrv  45762  monoord2xrv  45764  fmul01lt1lem1  45867  dvnmptdivc  46219  dvnmul  46224  itgspltprt  46260  stoweidlem17  46298  stoweidlem20  46301  stoweidlem34  46315  fourierdlem15  46403  fourierdlem48  46435  fourierdlem50  46437  fourierdlem52  46439  fourierdlem54  46441  fourierdlem64  46451  fourierdlem81  46468  fourierdlem102  46489  fourierdlem103  46490  fourierdlem104  46491  fourierdlem111  46498  fourierdlem114  46501  etransclem10  46525  etransclem14  46529  etransclem15  46530  etransclem24  46539  etransclem35  46550  etransclem44  46559  smfmullem4  47075  ssfz12  47597  smonoord  47654  gpg5grlim  48376  gpg5grlic  48377