Theorem eluzfz1 13537

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

Syntax hints:   → wi 4   ∈ wcel 2107  ‘cfv 6527  (class class class)co 7399  ℤcz 12580  ℤ_≥cuz 12844  ...cfz 13513

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-sep 5263  ax-nul 5273  ax-pow 5332  ax-pr 5399  ax-un 7723  ax-cnex 11177  ax-resscn 11178  ax-pre-lttri 11195

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ne 2932  df-nel 3036  df-ral 3051  df-rex 3060  df-rab 3414  df-v 3459  df-sbc 3764  df-csb 3873  df-dif 3927  df-un 3929  df-in 3931  df-ss 3941  df-nul 4307  df-if 4499  df-pw 4575  df-sn 4600  df-pr 4602  df-op 4606  df-uni 4881  df-iun 4966  df-br 5117  df-opab 5179  df-mpt 5199  df-id 5545  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6480  df-fun 6529  df-fn 6530  df-f 6531  df-f1 6532  df-fo 6533  df-f1o 6534  df-fv 6535  df-ov 7402  df-oprab 7403  df-mpo 7404  df-1st 7982  df-2nd 7983  df-er 8713  df-en 8954  df-dom 8955  df-sdom 8956  df-pnf 11263  df-mnf 11264  df-xr 11265  df-ltxr 11266  df-le 11267  df-neg 11461  df-z 12581  df-uz 12845  df-fz 13514

This theorem is referenced by:  elfz3  13540  fzn0  13544  fzopth  13567  seqcl  14029  seqfveq  14033  seqshft2  14035  monoord  14039  monoord2  14040  seqcaopr3  14044  seqf1olem2a  14047  seqf1olem2  14049  seqhomo  14056  seqcoll  14470  fsum1p  15756  telfsumo  15805  telfsumo2  15806  fsumparts  15809  mertenslem2  15888  prodfn0  15897  prodfrec  15898  fprod1p  15971  phicl2  16772  eulerthlem2  16786  4sqlem19  16968  vdwlem1  16986  vdwlem6  16991  vdw  16999  fvprmselelfz  17049  prmodvdslcmf  17052  gsumval2  18649  gsumsplit1r  18650  efgsdmi  19698  gsumval3  19873  telgsumfzslem  19954  telgsumfzs  19955  pmatcollpw3fi1lem1  22709  chfacfisf  22777  chfacfisfcpmat  22778  cpmadugsumlemF  22799  imasdsf1olem  24297  ovoliunlem1  25440  mbfi1fseqlem3  25655  cxpeq  26703  ppiltx  27123  logexprlim  27172  dchrmusum2  27441  dchrvmasum2lem  27443  mudivsum  27477  mulogsum  27479  mulog2sumlem2  27482  axlowdimlem13  28865  axlowdim1  28870  axlowdim  28872  crctcshwlkn0lem6  29729  fzto1stfv1  33030  fzto1stinvn  33033  cycpmco2f1  33053  lmatfval  33753  lmat22e11  33757  ballotlem4  34439  ballotlemic  34447  ballotlem1c  34448  ballotlem1ri  34475  subfacp1lem1  35122  subfacp1lem5  35127  subfacp1lem6  35128  cvmliftlem10  35237  cvmliftlem13  35239  inffz  35668  fwddifnp1  36104  poimirlem6  37571  poimirlem7  37572  poimirlem16  37581  poimirlem17  37582  poimirlem19  37584  poimirlem28  37593  fdc  37690  mettrifi  37702  sticksstones12a  42092  monoordxrv  45436  monoord2xrv  45438  fmul01lt1lem1  45543  dvnmptdivc  45897  dvnmul  45902  itgspltprt  45938  stoweidlem17  45976  stoweidlem20  45979  stoweidlem34  45993  fourierdlem15  46081  fourierdlem48  46113  fourierdlem50  46115  fourierdlem52  46117  fourierdlem54  46119  fourierdlem64  46129  fourierdlem81  46146  fourierdlem102  46167  fourierdlem103  46168  fourierdlem104  46169  fourierdlem111  46176  fourierdlem114  46179  etransclem10  46203  etransclem14  46207  etransclem15  46208  etransclem24  46217  etransclem35  46228  etransclem44  46237  smfmullem4  46753  ssfz12  47271  smonoord  47303  gpg5grlic  47992