Theorem eluzfz1 13480

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 12788	. . 3 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ)
2		uzid 12798	. . 3 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ≥‘𝑀))
3	1, 2	syl 17	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ (ℤ≥‘𝑀))
4		eluzfz 13468	. 2 ⊢ ((𝑀 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝑀)) → 𝑀 ∈ (𝑀...𝑁))
5	3, 4	mpancom 695	1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ (𝑀...𝑁))

Syntax hints:   → wi 4   ∈ wcel 2121  ‘cfv 6489  (class class class)co 7360  ℤcz 12519  ℤ_≥cuz 12783  ...cfz 13456

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-10 2154  ax-11 2170  ax-12 2191  ax-ext 2713  ax-sep 5221  ax-nul 5231  ax-pow 5297  ax-pr 5365  ax-un 7682  ax-cnex 11089  ax-resscn 11090  ax-pre-lttri 11107

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3or 1094  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-nf 1792  df-sb 2075  df-mo 2545  df-eu 2575  df-clab 2720  df-cleq 2733  df-clel 2816  df-nfc 2890  df-ne 2937  df-nel 3041  df-ral 3056  df-rex 3066  df-rab 3394  df-v 3435  df-sbc 3726  df-csb 3834  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4265  df-if 4458  df-pw 4534  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4842  df-iun 4926  df-br 5076  df-opab 5138  df-mpt 5157  df-id 5516  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496  df-fv 6497  df-ov 7363  df-oprab 7364  df-mpo 7365  df-1st 7935  df-2nd 7936  df-er 8637  df-en 8888  df-dom 8889  df-sdom 8890  df-pnf 11176  df-mnf 11177  df-xr 11178  df-ltxr 11179  df-le 11180  df-neg 11375  df-z 12520  df-uz 12784  df-fz 13457

This theorem is referenced by:  elfz3  13483  fzn0  13487  fzopth  13510  seqcl  13979  seqfveq  13983  seqshft2  13985  monoord  13989  monoord2  13990  seqcaopr3  13994  seqf1olem2a  13997  seqf1olem2  13999  seqhomo  14006  seqcoll  14421  fsum1p  15710  telfsumo  15760  telfsumo2  15761  fsumparts  15764  mertenslem2  15845  prodfn0  15854  prodfrec  15855  fprod1p  15928  phicl2  16733  eulerthlem2  16747  4sqlem19  16929  vdwlem1  16947  vdwlem6  16952  vdw  16960  fvprmselelfz  17010  prmodvdslcmf  17013  gsumval2  18649  gsumsplit1r  18650  efgsdmi  19702  gsumval3  19877  telgsumfzslem  19958  telgsumfzs  19959  pmatcollpw3fi1lem1  22773  chfacfisf  22841  chfacfisfcpmat  22842  cpmadugsumlemF  22863  imasdsf1olem  24360  ovoliunlem1  25491  mbfi1fseqlem3  25706  cxpeq  26743  ppiltx  27162  logexprlim  27210  dchrmusum2  27479  dchrvmasum2lem  27481  mudivsum  27515  mulogsum  27517  mulog2sumlem2  27520  axlowdimlem13  29045  axlowdim1  29050  axlowdim  29052  crctcshwlkn0lem6  29905  gsummptfzsplitla  33144  fzto1stfv1  33186  fzto1stinvn  33189  cycpmco2f1  33209  lmatfval  34010  lmat22e11  34014  ballotlem4  34695  ballotlemic  34703  ballotlem1c  34704  ballotlem1ri  34731  subfacp1lem1  35422  subfacp1lem5  35427  subfacp1lem6  35428  cvmliftlem10  35537  cvmliftlem13  35539  inffz  35973  fwddifnp1  36408  poimirlem6  38008  poimirlem7  38009  poimirlem16  38018  poimirlem17  38019  poimirlem19  38021  poimirlem28  38030  fdc  38127  mettrifi  38139  sticksstones12a  42657  monoordxrv  45938  monoord2xrv  45940  fmul01lt1lem1  46043  dvnmptdivc  46395  dvnmul  46400  itgspltprt  46436  stoweidlem17  46474  stoweidlem20  46477  stoweidlem34  46491  fourierdlem15  46579  fourierdlem48  46611  fourierdlem50  46613  fourierdlem52  46615  fourierdlem54  46617  fourierdlem64  46627  fourierdlem81  46644  fourierdlem102  46665  fourierdlem103  46666  fourierdlem104  46667  fourierdlem111  46674  fourierdlem114  46677  etransclem10  46701  etransclem14  46705  etransclem15  46706  etransclem24  46715  etransclem35  46726  etransclem44  46735  smfmullem4  47251  ssfz12  47791  smonoord  47854  gpg5grlim  48598  gpg5grlic  48599