Theorem eluzfz1 13471

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

Syntax hints:   → wi 4   ∈ wcel 2109  ‘cfv 6500  (class class class)co 7370  ℤcz 12508  ℤ_≥cuz 12772  ...cfz 13447

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 7692  ax-cnex 11103  ax-resscn 11104  ax-pre-lttri 11121

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 6453  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-ov 7373  df-oprab 7374  df-mpo 7375  df-1st 7948  df-2nd 7949  df-er 8649  df-en 8897  df-dom 8898  df-sdom 8899  df-pnf 11189  df-mnf 11190  df-xr 11191  df-ltxr 11192  df-le 11193  df-neg 11387  df-z 12509  df-uz 12773  df-fz 13448

This theorem is referenced by:  elfz3  13474  fzn0  13478  fzopth  13501  seqcl  13966  seqfveq  13970  seqshft2  13972  monoord  13976  monoord2  13977  seqcaopr3  13981  seqf1olem2a  13984  seqf1olem2  13986  seqhomo  13993  seqcoll  14408  fsum1p  15697  telfsumo  15746  telfsumo2  15747  fsumparts  15750  mertenslem2  15829  prodfn0  15838  prodfrec  15839  fprod1p  15912  phicl2  16716  eulerthlem2  16730  4sqlem19  16912  vdwlem1  16930  vdwlem6  16935  vdw  16943  fvprmselelfz  16993  prmodvdslcmf  16996  gsumval2  18597  gsumsplit1r  18598  efgsdmi  19648  gsumval3  19823  telgsumfzslem  19904  telgsumfzs  19905  pmatcollpw3fi1lem1  22708  chfacfisf  22776  chfacfisfcpmat  22777  cpmadugsumlemF  22798  imasdsf1olem  24296  ovoliunlem1  25438  mbfi1fseqlem3  25653  cxpeq  26702  ppiltx  27122  logexprlim  27171  dchrmusum2  27440  dchrvmasum2lem  27442  mudivsum  27476  mulogsum  27478  mulog2sumlem2  27481  axlowdimlem13  28936  axlowdim1  28941  axlowdim  28943  crctcshwlkn0lem6  29797  fzto1stfv1  33075  fzto1stinvn  33078  cycpmco2f1  33098  lmatfval  33799  lmat22e11  33803  ballotlem4  34485  ballotlemic  34493  ballotlem1c  34494  ballotlem1ri  34521  subfacp1lem1  35161  subfacp1lem5  35166  subfacp1lem6  35167  cvmliftlem10  35276  cvmliftlem13  35278  inffz  35712  fwddifnp1  36148  poimirlem6  37615  poimirlem7  37616  poimirlem16  37625  poimirlem17  37626  poimirlem19  37628  poimirlem28  37637  fdc  37734  mettrifi  37746  sticksstones12a  42140  monoordxrv  45472  monoord2xrv  45474  fmul01lt1lem1  45577  dvnmptdivc  45931  dvnmul  45936  itgspltprt  45972  stoweidlem17  46010  stoweidlem20  46013  stoweidlem34  46027  fourierdlem15  46115  fourierdlem48  46147  fourierdlem50  46149  fourierdlem52  46151  fourierdlem54  46153  fourierdlem64  46163  fourierdlem81  46180  fourierdlem102  46201  fourierdlem103  46202  fourierdlem104  46203  fourierdlem111  46210  fourierdlem114  46213  etransclem10  46237  etransclem14  46241  etransclem15  46242  etransclem24  46251  etransclem35  46262  etransclem44  46271  smfmullem4  46787  ssfz12  47310  smonoord  47367  gpg5grlic  48079