Theorem eluzfz1 13470

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

Syntax hints:   → wi 4   ∈ wcel 2109  ‘cfv 6499  (class class class)co 7369  ℤcz 12507  ℤ_≥cuz 12771  ...cfz 13446

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 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7691  ax-cnex 11102  ax-resscn 11103  ax-pre-lttri 11120

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 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-iun 4953  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-ov 7372  df-oprab 7373  df-mpo 7374  df-1st 7947  df-2nd 7948  df-er 8648  df-en 8896  df-dom 8897  df-sdom 8898  df-pnf 11188  df-mnf 11189  df-xr 11190  df-ltxr 11191  df-le 11192  df-neg 11386  df-z 12508  df-uz 12772  df-fz 13447

This theorem is referenced by:  elfz3  13473  fzn0  13477  fzopth  13500  seqcl  13965  seqfveq  13969  seqshft2  13971  monoord  13975  monoord2  13976  seqcaopr3  13980  seqf1olem2a  13983  seqf1olem2  13985  seqhomo  13992  seqcoll  14407  fsum1p  15696  telfsumo  15745  telfsumo2  15746  fsumparts  15749  mertenslem2  15828  prodfn0  15837  prodfrec  15838  fprod1p  15911  phicl2  16715  eulerthlem2  16729  4sqlem19  16911  vdwlem1  16929  vdwlem6  16934  vdw  16942  fvprmselelfz  16992  prmodvdslcmf  16995  gsumval2  18596  gsumsplit1r  18597  efgsdmi  19647  gsumval3  19822  telgsumfzslem  19903  telgsumfzs  19904  pmatcollpw3fi1lem1  22707  chfacfisf  22775  chfacfisfcpmat  22776  cpmadugsumlemF  22797  imasdsf1olem  24295  ovoliunlem1  25437  mbfi1fseqlem3  25652  cxpeq  26701  ppiltx  27121  logexprlim  27170  dchrmusum2  27439  dchrvmasum2lem  27441  mudivsum  27475  mulogsum  27477  mulog2sumlem2  27480  axlowdimlem13  28935  axlowdim1  28940  axlowdim  28942  crctcshwlkn0lem6  29796  fzto1stfv1  33074  fzto1stinvn  33077  cycpmco2f1  33097  lmatfval  33798  lmat22e11  33802  ballotlem4  34484  ballotlemic  34492  ballotlem1c  34493  ballotlem1ri  34520  subfacp1lem1  35160  subfacp1lem5  35165  subfacp1lem6  35166  cvmliftlem10  35275  cvmliftlem13  35277  inffz  35711  fwddifnp1  36147  poimirlem6  37614  poimirlem7  37615  poimirlem16  37624  poimirlem17  37625  poimirlem19  37627  poimirlem28  37636  fdc  37733  mettrifi  37745  sticksstones12a  42139  monoordxrv  45471  monoord2xrv  45473  fmul01lt1lem1  45576  dvnmptdivc  45930  dvnmul  45935  itgspltprt  45971  stoweidlem17  46009  stoweidlem20  46012  stoweidlem34  46026  fourierdlem15  46114  fourierdlem48  46146  fourierdlem50  46148  fourierdlem52  46150  fourierdlem54  46152  fourierdlem64  46162  fourierdlem81  46179  fourierdlem102  46200  fourierdlem103  46201  fourierdlem104  46202  fourierdlem111  46209  fourierdlem114  46212  etransclem10  46236  etransclem14  46240  etransclem15  46241  etransclem24  46250  etransclem35  46261  etransclem44  46270  smfmullem4  46786  ssfz12  47309  smonoord  47366  gpg5grlic  48078