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

Theorem eluzfz2 12387
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 11735 . . 3 (𝑁 ∈ (ℤ𝑀) → 𝑁 ∈ ℤ)
2 uzid 11740 . . 3 (𝑁 ∈ ℤ → 𝑁 ∈ (ℤ𝑁))
31, 2syl 17 . 2 (𝑁 ∈ (ℤ𝑀) → 𝑁 ∈ (ℤ𝑁))
4 eluzfz 12375 . 2 ((𝑁 ∈ (ℤ𝑀) ∧ 𝑁 ∈ (ℤ𝑁)) → 𝑁 ∈ (𝑀...𝑁))
53, 4mpdan 703 1 (𝑁 ∈ (ℤ𝑀) → 𝑁 ∈ (𝑀...𝑁))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2030  cfv 5926  (class class class)co 6690  cz 11415  cuz 11725  ...cfz 12364
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031  ax-pre-lttri 10048
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-1st 7210  df-2nd 7211  df-er 7787  df-en 7998  df-dom 7999  df-sdom 8000  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-neg 10307  df-z 11416  df-uz 11726  df-fz 12365
This theorem is referenced by:  eluzfz2b  12388  elfzubelfz  12391  fzopth  12416  fzsuc  12426  fseq1p1m1  12452  fzm1  12458  fzneuz  12459  fzoend  12599  uzindi  12821  seqcl2  12859  seqfveq2  12863  seqshft2  12867  monoord  12871  monoord2  12872  seqsplit  12874  seqcaopr3  12876  seqf1olem2a  12879  seqf1olem1  12880  seqf1olem2  12881  seqid2  12887  seqhomo  12888  seqcoll  13286  seqcoll2  13287  wrdeqs1cat  13520  swrdccatin12lem2  13535  swrdccatin12lem3  13536  swrdccatin12  13537  splid  13550  spllen  13551  splval2  13554  summolem2a  14490  fsumm1  14524  telfsumo  14578  telfsumo2  14579  fsumparts  14582  prodfn0  14670  prodfrec  14671  prodmolem2a  14708  fprodm1  14741  sadadd  15236  sadass  15240  smuval2  15251  vdwlem6  15737  efgredleme  18202  efgredlemc  18204  efgcpbllemb  18214  frgpuplem  18231  telgsumfzslem  18431  telgsumfzs  18432  pmatcollpw3fi1lem1  20639  chfacfisf  20707  chfacfisfcpmat  20708  iscmet3lem1  23135  iscmet3lem2  23136  voliunlem1  23364  volsup  23370  mbfi1fseqlem3  23529  wilthlem2  24840  wilthlem3  24841  chtub  24982  dchrisum0flb  25244  pntpbnd1  25320  pntlemf  25339  spthonepeq  26704  wwlksnext  26856  submatres  30000  madjusmdetlem1  30021  madjusmdetlem2  30022  madjusmdetlem3  30023  madjusmdetlem4  30024  ballotlemfc0  30682  ballotlemfcc  30683  ballotlemfrci  30717  gsumnunsn  30743  wrdsplex  30746  cvmliftlem10  31402  supfz  31739  fwddifnp1  32397  poimirlem3  33542  poimirlem4  33543  poimirlem16  33555  poimirlem19  33558  poimirlem20  33559  poimirlem23  33562  poimirlem31  33570  volsupnfl  33584  sdclem2  33668  fdc  33671  mettrifi  33683  iunincfi  39586  monoordxrv  40025  monoord2xrv  40027  fmul01lt1lem2  40135  limsupubuzlem  40262  dvnmul  40476  dvnprodlem3  40481  stoweidlem3  40538  stoweidlem11  40546  stoweidlem17  40552  stoweidlem34  40569  fourierdlem15  40657  fourierdlem25  40667  fourierdlem50  40691  fourierdlem52  40693  fourierdlem54  40695  fourierdlem65  40706  fourierdlem81  40722  fourierdlem92  40733  fourierdlem102  40743  fourierdlem111  40752  fourierdlem113  40754  fourierdlem114  40755  etransclem35  40804  sge0p1  40949  carageniuncllem1  41056  caratheodorylem1  41061  smfmullem4  41322  ssfz12  41649  elfzlble  41655  smonoord  41666  pfxccatin12lem2  41749  pfxccatin12  41750
  Copyright terms: Public domain W3C validator