Theorem eluzfz1 12665

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 11997	. . 3 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ)
2		uzid 12007	. . 3 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ≥‘𝑀))
3	1, 2	syl 17	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ (ℤ≥‘𝑀))
4		eluzfz 12654	. 2 ⊢ ((𝑀 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝑀)) → 𝑀 ∈ (𝑀...𝑁))
5	3, 4	mpancom 678	1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ (𝑀...𝑁))

Syntax hints:   → wi 4   ∈ wcel 2107  ‘cfv 6135  (class class class)co 6922  ℤcz 11728  ℤ_≥cuz 11992  ...cfz 12643

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226  ax-cnex 10328  ax-resscn 10329  ax-pre-lttri 10346

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-nel 3076  df-ral 3095  df-rex 3096  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4672  df-iun 4755  df-br 4887  df-opab 4949  df-mpt 4966  df-id 5261  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-iota 6099  df-fun 6137  df-fn 6138  df-f 6139  df-f1 6140  df-fo 6141  df-f1o 6142  df-fv 6143  df-ov 6925  df-oprab 6926  df-mpt2 6927  df-1st 7445  df-2nd 7446  df-er 8026  df-en 8242  df-dom 8243  df-sdom 8244  df-pnf 10413  df-mnf 10414  df-xr 10415  df-ltxr 10416  df-le 10417  df-neg 10609  df-z 11729  df-uz 11993  df-fz 12644

This theorem is referenced by:  elfz3  12668  fzn0  12672  fzopth  12695  seqcl  13139  seqfveq  13143  seqshft2  13145  monoord  13149  monoord2  13150  seqcaopr3  13154  seqf1olem2a  13157  seqf1olem2  13159  seqhomo  13166  seqcoll  13562  swrd0valOLD  13737  splidOLD  13895  spllenOLD  13897  splfv1OLD  13899  splfv2aOLD  13901  splval2OLD  13903  fsum1p  14889  telfsumo  14938  telfsumo2  14939  fsumparts  14942  mertenslem2  15020  prodfn0  15029  prodfrec  15030  fprod1p  15101  phicl2  15877  eulerthlem2  15891  4sqlem19  16071  vdwlem1  16089  vdwlem6  16094  vdw  16102  fvprmselelfz  16152  prmodvdslcmf  16155  gsumval2  17666  efgsdmi  18529  gsumval3  18694  telgsumfzslem  18772  telgsumfzs  18773  pmatcollpw3fi1lem1  20998  chfacfisf  21066  chfacfisfcpmat  21067  cpmadugsumlemF  21088  imasdsf1olem  22586  ovoliunlem1  23706  mbfi1fseqlem3  23921  cxpeq  24938  ppiltx  25355  logexprlim  25402  dchrmusum2  25635  dchrvmasum2lem  25637  mudivsum  25671  mulogsum  25673  mulog2sumlem2  25676  axlowdimlem13  26303  axlowdim1  26308  axlowdim  26310  crctcshwlkn0lem6  27164  fzto1stfv1  30449  fzto1stinvn  30452  lmatfval  30478  lmat22e11  30482  ballotlem4  31159  ballotlemic  31167  ballotlem1c  31168  ballotlem1ri  31195  wrdsplexOLD  31218  subfacp1lem1  31760  subfacp1lem5  31765  subfacp1lem6  31766  cvmliftlem10  31875  cvmliftlem13  31877  inffz  32209  fwddifnp1  32861  poimirlem6  34041  poimirlem7  34042  poimirlem16  34051  poimirlem17  34052  poimirlem19  34054  poimirlem28  34063  fdc  34165  mettrifi  34177  monoordxrv  40617  monoord2xrv  40619  fmul01lt1lem1  40724  dvnmptdivc  41081  dvnmul  41086  itgspltprt  41122  stoweidlem17  41161  stoweidlem20  41164  stoweidlem34  41178  fourierdlem15  41266  fourierdlem48  41298  fourierdlem50  41300  fourierdlem52  41302  fourierdlem54  41304  fourierdlem64  41314  fourierdlem81  41331  fourierdlem102  41352  fourierdlem103  41353  fourierdlem104  41354  fourierdlem111  41361  fourierdlem114  41364  etransclem10  41388  etransclem14  41392  etransclem15  41393  etransclem24  41402  etransclem35  41413  etransclem44  41422  smfmullem4  41928  ssfz12  42356  smonoord  42373