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

Theorem eluzfz1 12298
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
StepHypRef Expression
1 eluzel2 11644 . . 3 (𝑁 ∈ (ℤ𝑀) → 𝑀 ∈ ℤ)
2 uzid 11654 . . 3 (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ𝑀))
31, 2syl 17 . 2 (𝑁 ∈ (ℤ𝑀) → 𝑀 ∈ (ℤ𝑀))
4 eluzfz 12287 . 2 ((𝑀 ∈ (ℤ𝑀) ∧ 𝑁 ∈ (ℤ𝑀)) → 𝑀 ∈ (𝑀...𝑁))
53, 4mpancom 702 1 (𝑁 ∈ (ℤ𝑀) → 𝑀 ∈ (𝑀...𝑁))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1987  cfv 5852  (class class class)co 6610  cz 11329  cuz 11639  ...cfz 12276
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909  ax-cnex 9944  ax-resscn 9945  ax-pre-lttri 9962
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-op 4160  df-uni 4408  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-id 4994  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-ov 6613  df-oprab 6614  df-mpt2 6615  df-1st 7120  df-2nd 7121  df-er 7694  df-en 7908  df-dom 7909  df-sdom 7910  df-pnf 10028  df-mnf 10029  df-xr 10030  df-ltxr 10031  df-le 10032  df-neg 10221  df-z 11330  df-uz 11640  df-fz 12277
This theorem is referenced by:  elfz3  12301  fzn0  12305  fzopth  12328  seqcl  12769  seqfveq  12773  seqshft2  12775  monoord  12779  monoord2  12780  seqcaopr3  12784  seqf1olem2a  12787  seqf1olem2  12789  seqhomo  12796  seqcoll  13194  swrd0val  13367  splid  13449  spllen  13450  splfv1  13451  splfv2a  13452  splval2  13453  fsum1p  14423  telfsumo  14472  telfsumo2  14473  fsumparts  14476  mertenslem2  14553  prodfn0  14562  prodfrec  14563  fprod1p  14634  phicl2  15408  eulerthlem2  15422  4sqlem19  15602  vdwlem1  15620  vdwlem6  15625  vdw  15633  fvprmselelfz  15683  prmodvdslcmf  15686  gsumval2  17212  efgsdmi  18077  efgredleme  18088  efgredlemc  18090  efgcpbllemb  18100  frgpuplem  18117  gsumval3  18240  telgsumfzslem  18317  telgsumfzs  18318  pmatcollpw3fi1lem1  20523  chfacfisf  20591  chfacfisfcpmat  20592  cpmadugsumlemF  20613  imasdsf1olem  22101  ovoliunlem1  23193  mbfi1fseqlem3  23407  cxpeq  24415  ppiltx  24820  logexprlim  24867  dchrmusum2  25100  dchrvmasum2lem  25102  mudivsum  25136  mulogsum  25138  mulog2sumlem2  25141  axlowdimlem13  25751  axlowdim1  25756  axlowdim  25758  crctcshwlkn0lem6  26593  fzto1stfv1  29660  fzto1stinvn  29663  lmatfval  29686  lmat22e11  29690  ballotlem4  30365  ballotlemic  30373  ballotlem1c  30374  ballotlem1ri  30401  wrdsplex  30422  subfacp1lem1  30904  subfacp1lem5  30909  subfacp1lem6  30910  cvmliftlem10  31019  cvmliftlem13  31021  inffz  31357  inffzOLD  31358  fwddifnp1  31949  poimirlem6  33082  poimirlem7  33083  poimirlem16  33092  poimirlem17  33093  poimirlem19  33095  poimirlem28  33104  fdc  33208  mettrifi  33220  fmul01lt1lem1  39248  dvnmptdivc  39486  dvnmul  39491  itgspltprt  39528  stoweidlem17  39567  stoweidlem20  39570  stoweidlem34  39584  fourierdlem15  39672  fourierdlem48  39704  fourierdlem50  39706  fourierdlem52  39708  fourierdlem54  39710  fourierdlem64  39720  fourierdlem81  39737  fourierdlem102  39758  fourierdlem103  39759  fourierdlem104  39760  fourierdlem111  39767  fourierdlem114  39770  etransclem10  39794  etransclem14  39798  etransclem15  39799  etransclem24  39808  etransclem35  39819  etransclem44  39828  smfmullem4  40334  ssfz12  40647  smonoord  40665
  Copyright terms: Public domain W3C validator