Theorem eluzfz1 13434

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 12740	. . 3 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ)
2		uzid 12750	. . 3 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ≥‘𝑀))
3	1, 2	syl 17	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ (ℤ≥‘𝑀))
4		eluzfz 13422	. 2 ⊢ ((𝑀 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝑀)) → 𝑀 ∈ (𝑀...𝑁))
5	3, 4	mpancom 688	1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ (𝑀...𝑁))

Syntax hints:   → wi 4   ∈ wcel 2109  ‘cfv 6482  (class class class)co 7349  ℤcz 12471  ℤ_≥cuz 12735  ...cfz 13410

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pow 5304  ax-pr 5371  ax-un 7671  ax-cnex 11065  ax-resscn 11066  ax-pre-lttri 11083

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-iun 4943  df-br 5093  df-opab 5155  df-mpt 5174  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-iota 6438  df-fun 6484  df-fn 6485  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489  df-fv 6490  df-ov 7352  df-oprab 7353  df-mpo 7354  df-1st 7924  df-2nd 7925  df-er 8625  df-en 8873  df-dom 8874  df-sdom 8875  df-pnf 11151  df-mnf 11152  df-xr 11153  df-ltxr 11154  df-le 11155  df-neg 11350  df-z 12472  df-uz 12736  df-fz 13411

This theorem is referenced by:  elfz3  13437  fzn0  13441  fzopth  13464  seqcl  13929  seqfveq  13933  seqshft2  13935  monoord  13939  monoord2  13940  seqcaopr3  13944  seqf1olem2a  13947  seqf1olem2  13949  seqhomo  13956  seqcoll  14371  fsum1p  15660  telfsumo  15709  telfsumo2  15710  fsumparts  15713  mertenslem2  15792  prodfn0  15801  prodfrec  15802  fprod1p  15875  phicl2  16679  eulerthlem2  16693  4sqlem19  16875  vdwlem1  16893  vdwlem6  16898  vdw  16906  fvprmselelfz  16956  prmodvdslcmf  16959  gsumval2  18560  gsumsplit1r  18561  efgsdmi  19611  gsumval3  19786  telgsumfzslem  19867  telgsumfzs  19868  pmatcollpw3fi1lem1  22671  chfacfisf  22739  chfacfisfcpmat  22740  cpmadugsumlemF  22761  imasdsf1olem  24259  ovoliunlem1  25401  mbfi1fseqlem3  25616  cxpeq  26665  ppiltx  27085  logexprlim  27134  dchrmusum2  27403  dchrvmasum2lem  27405  mudivsum  27439  mulogsum  27441  mulog2sumlem2  27444  axlowdimlem13  28903  axlowdim1  28908  axlowdim  28910  crctcshwlkn0lem6  29764  fzto1stfv1  33052  fzto1stinvn  33055  cycpmco2f1  33075  lmatfval  33797  lmat22e11  33801  ballotlem4  34483  ballotlemic  34491  ballotlem1c  34492  ballotlem1ri  34519  subfacp1lem1  35172  subfacp1lem5  35177  subfacp1lem6  35178  cvmliftlem10  35287  cvmliftlem13  35289  inffz  35723  fwddifnp1  36159  poimirlem6  37626  poimirlem7  37627  poimirlem16  37636  poimirlem17  37637  poimirlem19  37639  poimirlem28  37648  fdc  37745  mettrifi  37757  sticksstones12a  42150  monoordxrv  45480  monoord2xrv  45482  fmul01lt1lem1  45585  dvnmptdivc  45939  dvnmul  45944  itgspltprt  45980  stoweidlem17  46018  stoweidlem20  46021  stoweidlem34  46035  fourierdlem15  46123  fourierdlem48  46155  fourierdlem50  46157  fourierdlem52  46159  fourierdlem54  46161  fourierdlem64  46171  fourierdlem81  46188  fourierdlem102  46209  fourierdlem103  46210  fourierdlem104  46211  fourierdlem111  46218  fourierdlem114  46221  etransclem10  46245  etransclem14  46249  etransclem15  46250  etransclem24  46259  etransclem35  46270  etransclem44  46279  smfmullem4  46795  ssfz12  47318  smonoord  47375  gpg5grlim  48097  gpg5grlic  48098