Theorem eluzfz2 13588

Description: Membership in a finite set of sequential integers - special case. (Contributed by NM, 13-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)

Assertion

Ref	Expression
eluzfz2	⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ (𝑀...𝑁))

Proof of Theorem eluzfz2

Step	Hyp	Ref	Expression
1		eluzelz 12900	. . 3 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℤ)
2		uzid 12905	. . 3 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ (ℤ≥‘𝑁))
3	1, 2	syl 18	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ (ℤ≥‘𝑁))
4		eluzfz 13575	. 2 ⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝑁)) → 𝑁 ∈ (𝑀...𝑁))
5	3, 4	mpdan 700	1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ (𝑀...𝑁))

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ‘cfv 6537  (class class class)co 7416  ℤcz 12618  ℤ_≥cuz 12890  ...cfz 13563

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402  ax-un 7739  ax-cnex 11183  ax-resscn 11184  ax-pre-lttri 11201

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-nel 3064  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-iun 4956  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-ov 7419  df-oprab 7420  df-mpo 7421  df-1st 7989  df-2nd 7990  df-er 8699  df-en 8956  df-dom 8957  df-sdom 8958  df-pnf 11272  df-mnf 11273  df-xr 11274  df-ltxr 11275  df-le 11276  df-neg 11471  df-z 12619  df-uz 12891  df-fz 13564

This theorem is used by:  eluzfz2b  13589  elfzubelfz  13592  fzopth  13618  fzsuc  13628  fseq1p1m1  13655  fzm1  13664  fzneuz  13665  fzoend  13815  uzindi  14048  seqcl2  14086  seqfveq2  14090  seqshft2  14094  monoord  14098  monoord2  14099  seqsplit  14101  seqcaopr3  14103  seqf1olem2a  14106  seqf1olem1  14107  seqf1olem2  14108  seqid2  14114  seqhomo  14115  seqcoll  14531  seqcoll2  14532  wrdeqs1cat  14791  pfxccatin12lem2  14802  pfxccatin12lem3  14803  splid  14824  spllen  14825  splval2  14828  swrdrevpfx  14840  summolem2a  15803  fsumm1  15839  telfsumo  15891  telfsumo2  15892  fsumparts  15895  prodfn0  15985  prodfrec  15986  prodmolem2a  16025  fprodm1  16058  sadadd  16561  sadass  16565  smuval2  16576  vdwlem6  17082  efgredleme  19871  efgredlemc  19873  efgcpbllemb  19883  frgpuplem  19900  telgsumfzslem  20116  telgsumfzs  20117  pmatcollpw3fi1lem1  23012  chfacfisf  23080  chfacfisfcpmat  23081  iscmet3lem1  25520  iscmet3lem2  25521  voliunlem1  25779  volsup  25785  mbfi1fseqlem3  25946  wilthlem2  27303  wilthlem3  27304  chtub  27446  dchrisum0flb  27744  pntpbnd1  27820  pntlemf  27839  spthonepeq  30203  wwlksnext  30347  2clwwlk2clwwlklem  30812  clwwlknonclwlknonf1o  30828  wrdsplex  33369  gsummptfzsplitra  33485  cycpmco2f1  33551  submatres  34303  madjusmdetlem1  34324  madjusmdetlem2  34325  madjusmdetlem3  34326  madjusmdetlem4  34327  ballotlemfc0  34991  ballotlemfcc  34992  ballotlemfrci  35026  gsumnunsn  35039  cvmliftlem10  35860  supfz  36295  fwddifnp1  36732  poimirlem3  38359  poimirlem4  38360  poimirlem16  38372  poimirlem19  38375  poimirlem20  38376  poimirlem23  38379  poimirlem31  38387  volsupnfl  38401  sdclem2  38479  fdc  38482  mettrifi  38494  iunincfi  45913  monoordxrv  46296  monoord2xrv  46298  fmul01lt1lem2  46402  limsupubuzlem  46527  dvnmul  46758  dvnprodlem3  46763  stoweidlem3  46818  stoweidlem11  46826  stoweidlem17  46832  stoweidlem34  46849  fourierdlem15  46937  fourierdlem25  46947  fourierdlem50  46971  fourierdlem52  46973  fourierdlem54  46975  fourierdlem65  46986  fourierdlem81  47002  fourierdlem92  47013  fourierdlem102  47023  fourierdlem111  47032  fourierdlem113  47034  fourierdlem114  47035  etransclem35  47084  sge0p1  47229  carageniuncllem1  47336  caratheodorylem1  47341  smfmullem4  47609  ssfz12  48189  elfzlble  48195  smonoord  48252  gpg3kgrtriexlem5  48990  gpg5grlim  48996  gpg5grlic  48997