Theorem eluzfz1 13482

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

Syntax hints:   → wi 4   ∈ wcel 2114  ‘cfv 6496  (class class class)co 7364  ℤcz 12521  ℤ_≥cuz 12785  ...cfz 13458

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 5232  ax-nul 5242  ax-pow 5306  ax-pr 5374  ax-un 7686  ax-cnex 11091  ax-resscn 11092  ax-pre-lttri 11109

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 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5523  df-xp 5634  df-rel 5635  df-cnv 5636  df-co 5637  df-dm 5638  df-rn 5639  df-res 5640  df-ima 5641  df-iota 6452  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-ov 7367  df-oprab 7368  df-mpo 7369  df-1st 7939  df-2nd 7940  df-er 8640  df-en 8891  df-dom 8892  df-sdom 8893  df-pnf 11178  df-mnf 11179  df-xr 11180  df-ltxr 11181  df-le 11182  df-neg 11377  df-z 12522  df-uz 12786  df-fz 13459

This theorem is referenced by:  elfz3  13485  fzn0  13489  fzopth  13512  seqcl  13981  seqfveq  13985  seqshft2  13987  monoord  13991  monoord2  13992  seqcaopr3  13996  seqf1olem2a  13999  seqf1olem2  14001  seqhomo  14008  seqcoll  14423  fsum1p  15712  telfsumo  15762  telfsumo2  15763  fsumparts  15766  mertenslem2  15847  prodfn0  15856  prodfrec  15857  fprod1p  15930  phicl2  16735  eulerthlem2  16749  4sqlem19  16931  vdwlem1  16949  vdwlem6  16954  vdw  16962  fvprmselelfz  17012  prmodvdslcmf  17015  gsumval2  18651  gsumsplit1r  18652  efgsdmi  19704  gsumval3  19879  telgsumfzslem  19960  telgsumfzs  19961  pmatcollpw3fi1lem1  22767  chfacfisf  22835  chfacfisfcpmat  22836  cpmadugsumlemF  22857  imasdsf1olem  24354  ovoliunlem1  25485  mbfi1fseqlem3  25700  cxpeq  26740  ppiltx  27160  logexprlim  27208  dchrmusum2  27477  dchrvmasum2lem  27479  mudivsum  27513  mulogsum  27515  mulog2sumlem2  27518  axlowdimlem13  29043  axlowdim1  29048  axlowdim  29050  crctcshwlkn0lem6  29904  gsummptfzsplitla  33141  fzto1stfv1  33183  fzto1stinvn  33186  cycpmco2f1  33206  lmatfval  33980  lmat22e11  33984  ballotlem4  34665  ballotlemic  34673  ballotlem1c  34674  ballotlem1ri  34701  subfacp1lem1  35383  subfacp1lem5  35388  subfacp1lem6  35389  cvmliftlem10  35498  cvmliftlem13  35500  inffz  35934  fwddifnp1  36369  poimirlem6  37969  poimirlem7  37970  poimirlem16  37979  poimirlem17  37980  poimirlem19  37982  poimirlem28  37991  fdc  38088  mettrifi  38100  sticksstones12a  42618  monoordxrv  45935  monoord2xrv  45937  fmul01lt1lem1  46040  dvnmptdivc  46392  dvnmul  46397  itgspltprt  46433  stoweidlem17  46471  stoweidlem20  46474  stoweidlem34  46488  fourierdlem15  46576  fourierdlem48  46608  fourierdlem50  46610  fourierdlem52  46612  fourierdlem54  46614  fourierdlem64  46624  fourierdlem81  46641  fourierdlem102  46662  fourierdlem103  46663  fourierdlem104  46664  fourierdlem111  46671  fourierdlem114  46674  etransclem10  46698  etransclem14  46702  etransclem15  46703  etransclem24  46712  etransclem35  46723  etransclem44  46732  smfmullem4  47248  ssfz12  47782  smonoord  47845  gpg5grlim  48589  gpg5grlic  48590