Theorem eluzfz1 12908

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 12242	. . 3 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ)
2		uzid 12252	. . 3 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ≥‘𝑀))
3	1, 2	syl 17	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ (ℤ≥‘𝑀))
4		eluzfz 12897	. 2 ⊢ ((𝑀 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝑀)) → 𝑀 ∈ (𝑀...𝑁))
5	3, 4	mpancom 686	1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ (𝑀...𝑁))

Syntax hints:   → wi 4   ∈ wcel 2110  ‘cfv 6349  (class class class)co 7150  ℤcz 11975  ℤ_≥cuz 12237  ...cfz 12886

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7455  ax-cnex 10587  ax-resscn 10588  ax-pre-lttri 10605

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-pw 4540  df-sn 4561  df-pr 4563  df-op 4567  df-uni 4832  df-iun 4913  df-br 5059  df-opab 5121  df-mpt 5139  df-id 5454  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357  df-ov 7153  df-oprab 7154  df-mpo 7155  df-1st 7683  df-2nd 7684  df-er 8283  df-en 8504  df-dom 8505  df-sdom 8506  df-pnf 10671  df-mnf 10672  df-xr 10673  df-ltxr 10674  df-le 10675  df-neg 10867  df-z 11976  df-uz 12238  df-fz 12887

This theorem is referenced by:  elfz3  12911  fzn0  12915  fzopth  12938  seqcl  13384  seqfveq  13388  seqshft2  13390  monoord  13394  monoord2  13395  seqcaopr3  13399  seqf1olem2a  13402  seqf1olem2  13404  seqhomo  13411  seqcoll  13816  fsum1p  15102  telfsumo  15151  telfsumo2  15152  fsumparts  15155  mertenslem2  15235  prodfn0  15244  prodfrec  15245  fprod1p  15316  phicl2  16099  eulerthlem2  16113  4sqlem19  16293  vdwlem1  16311  vdwlem6  16316  vdw  16324  fvprmselelfz  16374  prmodvdslcmf  16377  gsumval2  17890  gsumsplit1r  17891  efgsdmi  18852  gsumval3  19021  telgsumfzslem  19102  telgsumfzs  19103  pmatcollpw3fi1lem1  21388  chfacfisf  21456  chfacfisfcpmat  21457  cpmadugsumlemF  21478  imasdsf1olem  22977  ovoliunlem1  24097  mbfi1fseqlem3  24312  cxpeq  25332  ppiltx  25748  logexprlim  25795  dchrmusum2  26064  dchrvmasum2lem  26066  mudivsum  26100  mulogsum  26102  mulog2sumlem2  26105  axlowdimlem13  26734  axlowdim1  26739  axlowdim  26741  crctcshwlkn0lem6  27587  fzto1stfv1  30738  fzto1stinvn  30741  cycpmco2f1  30761  lmatfval  31074  lmat22e11  31078  ballotlem4  31751  ballotlemic  31759  ballotlem1c  31760  ballotlem1ri  31787  subfacp1lem1  32421  subfacp1lem5  32426  subfacp1lem6  32427  cvmliftlem10  32536  cvmliftlem13  32538  inffz  32956  fwddifnp1  33621  poimirlem6  34892  poimirlem7  34893  poimirlem16  34902  poimirlem17  34903  poimirlem19  34905  poimirlem28  34914  fdc  35014  mettrifi  35026  monoordxrv  41751  monoord2xrv  41753  fmul01lt1lem1  41858  dvnmptdivc  42216  dvnmul  42221  itgspltprt  42257  stoweidlem17  42296  stoweidlem20  42299  stoweidlem34  42313  fourierdlem15  42401  fourierdlem48  42433  fourierdlem50  42435  fourierdlem52  42437  fourierdlem54  42439  fourierdlem64  42449  fourierdlem81  42466  fourierdlem102  42487  fourierdlem103  42488  fourierdlem104  42489  fourierdlem111  42496  fourierdlem114  42499  etransclem10  42523  etransclem14  42527  etransclem15  42528  etransclem24  42537  etransclem35  42548  etransclem44  42557  smfmullem4  43063  ssfz12  43508  smonoord  43525