Theorem eluzfz2 13665

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 12975	. . 3 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ ℤ)
2		uzid 12980	. . 3 ⊢ (𝑁 ∈ ℤ → 𝑁 ∈ (ℤ≥‘𝑁))
3	1, 2	syl 18	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ (ℤ≥‘𝑁))
4		eluzfz 13651	. 2 ⊢ ((𝑁 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝑁)) → 𝑁 ∈ (𝑀...𝑁))
5	3, 4	mpdan 700	1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑁 ∈ (𝑀...𝑁))

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  ‘cfv 6538  (class class class)co 7420  ℤcz 12693  ℤ_≥cuz 12965  ...cfz 13639

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7751  ax-cnex 11256  ax-resscn 11257  ax-pre-lttri 11274

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-ov 7423  df-oprab 7424  df-mpo 7425  df-1st 8001  df-2nd 8002  df-er 8717  df-en 8974  df-dom 8975  df-sdom 8976  df-pnf 11345  df-mnf 11346  df-xr 11347  df-ltxr 11348  df-le 11349  df-neg 11544  df-z 12694  df-uz 12966  df-fz 13640

This theorem is used by:  eluzfz2b  13666  elfzubelfz  13669  fzopth  13695  fzsuc  13705  fseq1p1m1  13732  fzm1  13741  fzneuz  13742  fzoend  13892  uzindi  14125  seqcl2  14163  seqfveq2  14167  seqshft2  14171  monoord  14175  monoord2  14176  seqsplit  14178  seqcaopr3  14180  seqf1olem2a  14183  seqf1olem1  14184  seqf1olem2  14185  seqid2  14191  seqhomo  14192  seqcoll  14609  seqcoll2  14610  wrdeqs1cat  14869  pfxccatin12lem2  14880  pfxccatin12lem3  14881  splid  14902  spllen  14903  splval2  14906  swrdrevpfx  14918  summolem2a  15881  fsumm1  15917  telfsumo  15969  telfsumo2  15970  fsumparts  15973  prodfn0  16063  prodfrec  16064  prodmolem2a  16101  fprodm1  16134  sadadd  16637  sadass  16641  smuval2  16652  vdwlem6  17164  efgredleme  19957  efgredlemc  19959  efgcpbllemb  19969  frgpuplem  19986  telgsumfzslem  20202  telgsumfzs  20203  pmatcollpw3fi1lem1  23104  chfacfisf  23172  chfacfisfcpmat  23173  iscmet3lem1  25612  iscmet3lem2  25613  voliunlem1  25871  volsup  25877  mbfi1fseqlem3  26038  wilthlem2  27396  wilthlem3  27397  chtub  27539  dchrisum0flb  27837  pntpbnd1  27913  pntlemf  27932  spthonepeq  30338  wwlksnext  30482  2clwwlk2clwwlklem  30947  clwwlknonclwlknonf1o  30963  wrdsplex  33503  gsummptfzsplitra  33619  cycpmco2f1  33685  submatres  34438  madjusmdetlem1  34459  madjusmdetlem2  34460  madjusmdetlem3  34461  madjusmdetlem4  34462  ballotlemfc0  35125  ballotlemfcc  35126  ballotlemfrci  35160  gsumnunsn  35173  cvmliftlem10  36059  supfz  36494  fwddifnp1  36930  poimirlem3  38542  poimirlem4  38543  poimirlem16  38555  poimirlem19  38558  poimirlem20  38559  poimirlem23  38562  poimirlem31  38570  volsupnfl  38584  sdclem2  38677  fdc  38680  mettrifi  38692  iunincfi  46109  monoordxrv  46491  monoord2xrv  46493  fmul01lt1lem2  46597  limsupubuzlem  46722  dvnmul  46953  dvnprodlem3  46958  stoweidlem3  47013  stoweidlem11  47021  stoweidlem17  47027  stoweidlem34  47044  fourierdlem15  47132  fourierdlem25  47142  fourierdlem50  47166  fourierdlem52  47168  fourierdlem54  47170  fourierdlem65  47181  fourierdlem81  47197  fourierdlem92  47208  fourierdlem102  47218  fourierdlem111  47227  fourierdlem113  47229  fourierdlem114  47230  etransclem35  47279  sge0p1  47424  carageniuncllem1  47531  caratheodorylem1  47536  smfmullem4  47804  ssfz12  48384  elfzlble  48390  smonoord  48447  gpg3kgrtriexlem5  49185  gpg5grlim  49191  gpg5grlic  49192