MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eluzfz2 Structured version   Visualization version   GIF version

Theorem eluzfz2 13125
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
StepHypRef Expression
1 eluzelz 12453 . . 3 (𝑁 ∈ (ℤ𝑀) → 𝑁 ∈ ℤ)
2 uzid 12458 . . 3 (𝑁 ∈ ℤ → 𝑁 ∈ (ℤ𝑁))
31, 2syl 17 . 2 (𝑁 ∈ (ℤ𝑀) → 𝑁 ∈ (ℤ𝑁))
4 eluzfz 13112 . 2 ((𝑁 ∈ (ℤ𝑀) ∧ 𝑁 ∈ (ℤ𝑁)) → 𝑁 ∈ (𝑀...𝑁))
53, 4mpdan 687 1 (𝑁 ∈ (ℤ𝑀) → 𝑁 ∈ (𝑀...𝑁))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2110  cfv 6385  (class class class)co 7218  cz 12181  cuz 12443  ...cfz 13100
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-sep 5197  ax-nul 5204  ax-pow 5263  ax-pr 5327  ax-un 7528  ax-cnex 10790  ax-resscn 10791  ax-pre-lttri 10808
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3415  df-sbc 3700  df-csb 3817  df-dif 3874  df-un 3876  df-in 3878  df-ss 3888  df-nul 4243  df-if 4445  df-pw 4520  df-sn 4547  df-pr 4549  df-op 4553  df-uni 4825  df-iun 4911  df-br 5059  df-opab 5121  df-mpt 5141  df-id 5460  df-xp 5562  df-rel 5563  df-cnv 5564  df-co 5565  df-dm 5566  df-rn 5567  df-res 5568  df-ima 5569  df-iota 6343  df-fun 6387  df-fn 6388  df-f 6389  df-f1 6390  df-fo 6391  df-f1o 6392  df-fv 6393  df-ov 7221  df-oprab 7222  df-mpo 7223  df-1st 7766  df-2nd 7767  df-er 8396  df-en 8632  df-dom 8633  df-sdom 8634  df-pnf 10874  df-mnf 10875  df-xr 10876  df-ltxr 10877  df-le 10878  df-neg 11070  df-z 12182  df-uz 12444  df-fz 13101
This theorem is referenced by:  eluzfz2b  13126  elfzubelfz  13129  fzopth  13154  fzsuc  13164  fseq1p1m1  13191  fzm1  13197  fzneuz  13198  fzoend  13338  uzindi  13560  seqcl2  13599  seqfveq2  13603  seqshft2  13607  monoord  13611  monoord2  13612  seqsplit  13614  seqcaopr3  13616  seqf1olem2a  13619  seqf1olem1  13620  seqf1olem2  13621  seqid2  13627  seqhomo  13628  seqcoll  14035  seqcoll2  14036  wrdeqs1cat  14290  pfxccatin12lem2  14301  pfxccatin12lem3  14302  splid  14323  spllen  14324  splval2  14327  summolem2a  15284  fsumm1  15320  telfsumo  15371  telfsumo2  15372  fsumparts  15375  prodfn0  15463  prodfrec  15464  prodmolem2a  15501  fprodm1  15534  sadadd  16031  sadass  16035  smuval2  16046  vdwlem6  16544  efgredleme  19138  efgredlemc  19140  efgcpbllemb  19150  frgpuplem  19167  telgsumfzslem  19378  telgsumfzs  19379  pmatcollpw3fi1lem1  21688  chfacfisf  21756  chfacfisfcpmat  21757  iscmet3lem1  24193  iscmet3lem2  24194  voliunlem1  24452  volsup  24458  mbfi1fseqlem3  24620  wilthlem2  25956  wilthlem3  25957  chtub  26098  dchrisum0flb  26396  pntpbnd1  26472  pntlemf  26491  spthonepeq  27844  wwlksnext  27982  2clwwlk2clwwlklem  28434  clwwlknonclwlknonf1o  28450  wrdsplex  30937  cycpmco2f1  31115  submatres  31475  madjusmdetlem1  31496  madjusmdetlem2  31497  madjusmdetlem3  31498  madjusmdetlem4  31499  ballotlemfc0  32176  ballotlemfcc  32177  ballotlemfrci  32211  gsumnunsn  32237  swrdrevpfx  32796  cvmliftlem10  32974  supfz  33417  fwddifnp1  34209  poimirlem3  35522  poimirlem4  35523  poimirlem16  35535  poimirlem19  35538  poimirlem20  35539  poimirlem23  35542  poimirlem31  35550  volsupnfl  35564  sdclem2  35642  fdc  35645  mettrifi  35657  iunincfi  42325  monoordxrv  42705  monoord2xrv  42707  fmul01lt1lem2  42809  limsupubuzlem  42936  dvnmul  43167  dvnprodlem3  43172  stoweidlem3  43227  stoweidlem11  43235  stoweidlem17  43241  stoweidlem34  43258  fourierdlem15  43346  fourierdlem25  43356  fourierdlem50  43380  fourierdlem52  43382  fourierdlem54  43384  fourierdlem65  43395  fourierdlem81  43411  fourierdlem92  43422  fourierdlem102  43432  fourierdlem111  43441  fourierdlem113  43443  fourierdlem114  43444  etransclem35  43493  sge0p1  43635  carageniuncllem1  43742  caratheodorylem1  43747  smfmullem4  44008  ssfz12  44487  elfzlble  44493  smonoord  44504
  Copyright terms: Public domain W3C validator