Theorem eluzfz1 13461

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

Syntax hints:   → wi 4   ∈ wcel 2114  ‘cfv 6502  (class class class)co 7370  ℤcz 12502  ℤ_≥cuz 12765  ...cfz 13437

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 2185  ax-ext 2709  ax-sep 5245  ax-nul 5255  ax-pow 5314  ax-pr 5381  ax-un 7692  ax-cnex 11096  ax-resscn 11097  ax-pre-lttri 11114

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 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5529  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-iota 6458  df-fun 6504  df-fn 6505  df-f 6506  df-f1 6507  df-fo 6508  df-f1o 6509  df-fv 6510  df-ov 7373  df-oprab 7374  df-mpo 7375  df-1st 7945  df-2nd 7946  df-er 8647  df-en 8898  df-dom 8899  df-sdom 8900  df-pnf 11182  df-mnf 11183  df-xr 11184  df-ltxr 11185  df-le 11186  df-neg 11381  df-z 12503  df-uz 12766  df-fz 13438

This theorem is referenced by:  elfz3  13464  fzn0  13468  fzopth  13491  seqcl  13959  seqfveq  13963  seqshft2  13965  monoord  13969  monoord2  13970  seqcaopr3  13974  seqf1olem2a  13977  seqf1olem2  13979  seqhomo  13986  seqcoll  14401  fsum1p  15690  telfsumo  15739  telfsumo2  15740  fsumparts  15743  mertenslem2  15822  prodfn0  15831  prodfrec  15832  fprod1p  15905  phicl2  16709  eulerthlem2  16723  4sqlem19  16905  vdwlem1  16923  vdwlem6  16928  vdw  16936  fvprmselelfz  16986  prmodvdslcmf  16989  gsumval2  18625  gsumsplit1r  18626  efgsdmi  19678  gsumval3  19853  telgsumfzslem  19934  telgsumfzs  19935  pmatcollpw3fi1lem1  22747  chfacfisf  22815  chfacfisfcpmat  22816  cpmadugsumlemF  22837  imasdsf1olem  24334  ovoliunlem1  25476  mbfi1fseqlem3  25691  cxpeq  26740  ppiltx  27160  logexprlim  27209  dchrmusum2  27478  dchrvmasum2lem  27480  mudivsum  27514  mulogsum  27516  mulog2sumlem2  27519  axlowdimlem13  29045  axlowdim1  29050  axlowdim  29052  crctcshwlkn0lem6  29906  gsummptfzsplitla  33159  fzto1stfv1  33201  fzto1stinvn  33204  cycpmco2f1  33224  lmatfval  33998  lmat22e11  34002  ballotlem4  34683  ballotlemic  34691  ballotlem1c  34692  ballotlem1ri  34719  subfacp1lem1  35401  subfacp1lem5  35406  subfacp1lem6  35407  cvmliftlem10  35516  cvmliftlem13  35518  inffz  35952  fwddifnp1  36387  poimirlem6  37906  poimirlem7  37907  poimirlem16  37916  poimirlem17  37917  poimirlem19  37919  poimirlem28  37928  fdc  38025  mettrifi  38037  sticksstones12a  42556  monoordxrv  45868  monoord2xrv  45870  fmul01lt1lem1  45973  dvnmptdivc  46325  dvnmul  46330  itgspltprt  46366  stoweidlem17  46404  stoweidlem20  46407  stoweidlem34  46421  fourierdlem15  46509  fourierdlem48  46541  fourierdlem50  46543  fourierdlem52  46545  fourierdlem54  46547  fourierdlem64  46557  fourierdlem81  46574  fourierdlem102  46595  fourierdlem103  46596  fourierdlem104  46597  fourierdlem111  46604  fourierdlem114  46607  etransclem10  46631  etransclem14  46635  etransclem15  46636  etransclem24  46645  etransclem35  46656  etransclem44  46665  smfmullem4  47181  ssfz12  47703  smonoord  47760  gpg5grlim  48482  gpg5grlic  48483