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

Theorem eluzfz1 12462
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 11805 . . 3 (𝑁 ∈ (ℤ𝑀) → 𝑀 ∈ ℤ)
2 uzid 11815 . . 3 (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ𝑀))
31, 2syl 17 . 2 (𝑁 ∈ (ℤ𝑀) → 𝑀 ∈ (ℤ𝑀))
4 eluzfz 12451 . 2 ((𝑀 ∈ (ℤ𝑀) ∧ 𝑁 ∈ (ℤ𝑀)) → 𝑀 ∈ (𝑀...𝑁))
53, 4mpancom 706 1 (𝑁 ∈ (ℤ𝑀) → 𝑀 ∈ (𝑀...𝑁))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2103  cfv 6001  (class class class)co 6765  cz 11490  cuz 11800  ...cfz 12440
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-8 2105  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704  ax-sep 4889  ax-nul 4897  ax-pow 4948  ax-pr 5011  ax-un 7066  ax-cnex 10105  ax-resscn 10106  ax-pre-lttri 10123
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-eu 2575  df-mo 2576  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-ne 2897  df-nel 3000  df-ral 3019  df-rex 3020  df-rab 3023  df-v 3306  df-sbc 3542  df-csb 3640  df-dif 3683  df-un 3685  df-in 3687  df-ss 3694  df-nul 4024  df-if 4195  df-pw 4268  df-sn 4286  df-pr 4288  df-op 4292  df-uni 4545  df-iun 4630  df-br 4761  df-opab 4821  df-mpt 4838  df-id 5128  df-xp 5224  df-rel 5225  df-cnv 5226  df-co 5227  df-dm 5228  df-rn 5229  df-res 5230  df-ima 5231  df-iota 5964  df-fun 6003  df-fn 6004  df-f 6005  df-f1 6006  df-fo 6007  df-f1o 6008  df-fv 6009  df-ov 6768  df-oprab 6769  df-mpt2 6770  df-1st 7285  df-2nd 7286  df-er 7862  df-en 8073  df-dom 8074  df-sdom 8075  df-pnf 10189  df-mnf 10190  df-xr 10191  df-ltxr 10192  df-le 10193  df-neg 10382  df-z 11491  df-uz 11801  df-fz 12441
This theorem is referenced by:  elfz3  12465  fzn0  12469  fzopth  12492  seqcl  12936  seqfveq  12940  seqshft2  12942  monoord  12946  monoord2  12947  seqcaopr3  12951  seqf1olem2a  12954  seqf1olem2  12956  seqhomo  12963  seqcoll  13361  swrd0val  13541  splid  13625  spllen  13626  splfv1  13627  splfv2a  13628  splval2  13629  fsum1p  14602  telfsumo  14654  telfsumo2  14655  fsumparts  14658  mertenslem2  14737  prodfn0  14746  prodfrec  14747  fprod1p  14818  phicl2  15596  eulerthlem2  15610  4sqlem19  15790  vdwlem1  15808  vdwlem6  15813  vdw  15821  fvprmselelfz  15871  prmodvdslcmf  15874  gsumval2  17402  efgsdmi  18266  efgredleme  18277  efgredlemc  18279  efgcpbllemb  18289  frgpuplem  18306  gsumval3  18429  telgsumfzslem  18506  telgsumfzs  18507  pmatcollpw3fi1lem1  20714  chfacfisf  20782  chfacfisfcpmat  20783  cpmadugsumlemF  20804  imasdsf1olem  22300  ovoliunlem1  23391  mbfi1fseqlem3  23604  cxpeq  24618  ppiltx  25023  logexprlim  25070  dchrmusum2  25303  dchrvmasum2lem  25305  mudivsum  25339  mulogsum  25341  mulog2sumlem2  25344  axlowdimlem13  25954  axlowdim1  25959  axlowdim  25961  crctcshwlkn0lem6  26839  fzto1stfv1  30081  fzto1stinvn  30084  lmatfval  30110  lmat22e11  30114  ballotlem4  30790  ballotlemic  30798  ballotlem1c  30799  ballotlem1ri  30826  wrdsplex  30848  subfacp1lem1  31389  subfacp1lem5  31394  subfacp1lem6  31395  cvmliftlem10  31504  cvmliftlem13  31506  inffz  31842  inffzOLD  31843  fwddifnp1  32499  poimirlem6  33647  poimirlem7  33648  poimirlem16  33657  poimirlem17  33658  poimirlem19  33660  poimirlem28  33669  fdc  33773  mettrifi  33785  monoordxrv  40127  monoord2xrv  40129  fmul01lt1lem1  40236  dvnmptdivc  40573  dvnmul  40578  itgspltprt  40615  stoweidlem17  40654  stoweidlem20  40657  stoweidlem34  40671  fourierdlem15  40759  fourierdlem48  40791  fourierdlem50  40793  fourierdlem52  40795  fourierdlem54  40797  fourierdlem64  40807  fourierdlem81  40824  fourierdlem102  40845  fourierdlem103  40846  fourierdlem104  40847  fourierdlem111  40854  fourierdlem114  40857  etransclem10  40881  etransclem14  40885  etransclem15  40886  etransclem24  40895  etransclem35  40906  etransclem44  40915  smfmullem4  41424  ssfz12  41751  smonoord  41768
  Copyright terms: Public domain W3C validator