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

Theorem eluzfz1 11024
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  |-  ( N  e.  ( ZZ>= `  M
)  ->  M  e.  ( M ... N ) )

Proof of Theorem eluzfz1
StepHypRef Expression
1 eluzel2 10453 . . 3  |-  ( N  e.  ( ZZ>= `  M
)  ->  M  e.  ZZ )
2 uzid 10460 . . 3  |-  ( M  e.  ZZ  ->  M  e.  ( ZZ>= `  M )
)
31, 2syl 16 . 2  |-  ( N  e.  ( ZZ>= `  M
)  ->  M  e.  ( ZZ>= `  M )
)
4 eluzfz 11014 . 2  |-  ( ( M  e.  ( ZZ>= `  M )  /\  N  e.  ( ZZ>= `  M )
)  ->  M  e.  ( M ... N ) )
53, 4mpancom 651 1  |-  ( N  e.  ( ZZ>= `  M
)  ->  M  e.  ( M ... N ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1721   ` cfv 5417  (class class class)co 6044   ZZcz 10242   ZZ>=cuz 10448   ...cfz 11003
This theorem is referenced by:  elfz3  11027  fzn0  11030  fzopth  11049  elfzp12  11085  seqcl  11302  seqfveq  11306  seqshft2  11308  monoord  11312  monoord2  11313  seqcaopr3  11317  seqf1olem2a  11320  seqf1olem2  11322  seqhomo  11329  bcn0  11560  seqcoll  11671  swrd0val  11727  swrdid  11731  splid  11741  spllen  11742  splfv1  11743  splfv2a  11744  splval2  11745  wrdeqcats1  11747  wrdeqs1cat  11748  fsum1p  12498  fsumtscopo  12540  fsumtscopo2  12541  fsumparts  12544  mertenslem2  12621  phicl2  13116  eulerthlem2  13130  4sqlem19  13290  vdwlem1  13308  vdwlem6  13313  vdw  13321  gsumval2  14742  efgsdmi  15323  efgredleme  15334  efgredlemc  15336  efgcpbllemb  15346  frgpuplem  15363  gsumval3  15473  imasdsf1olem  18360  ovoliunlem1  19355  mbfi1fseqlem3  19566  cxpeq  20598  ppiltx  20917  logexprlim  20966  dchrmusum2  21145  dchrvmasum2lem  21147  mudivsum  21181  mulogsum  21183  mulog2sumlem2  21186  spthonepeq  21544  constr3pthlem3  21601  eupath2  21659  konigsberg  21666  ballotlem4  24713  ballotlemic  24721  ballotlem1c  24722  ballotlem1ri  24749  subfacp1lem1  24822  subfacp1lem5  24827  subfacp1lem6  24828  cvmliftlem10  24938  cvmliftlem13  24940  inffz  25157  prodfn0  25179  prodfrec  25180  fprod1p  25248  axlowdimlem13  25801  axlowdim1  25806  axlowdim  25808  fdc  26343  mettrifi  26357  fmul01lt1lem1  27585  stoweidlem17  27637  stoweidlem20  27640  stoweidlem34  27654  ssfz12  27980  swrd0swrdid  28016  swrdccatin12b  28031  swrdccat3a  28034
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2389  ax-sep 4294  ax-nul 4302  ax-pow 4341  ax-pr 4367  ax-un 4664  ax-cnex 9006  ax-resscn 9007  ax-pre-lttri 9024
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2262  df-mo 2263  df-clab 2395  df-cleq 2401  df-clel 2404  df-nfc 2533  df-ne 2573  df-nel 2574  df-ral 2675  df-rex 2676  df-rab 2679  df-v 2922  df-sbc 3126  df-csb 3216  df-dif 3287  df-un 3289  df-in 3291  df-ss 3298  df-nul 3593  df-if 3704  df-pw 3765  df-sn 3784  df-pr 3785  df-op 3787  df-uni 3980  df-iun 4059  df-br 4177  df-opab 4231  df-mpt 4232  df-id 4462  df-xp 4847  df-rel 4848  df-cnv 4849  df-co 4850  df-dm 4851  df-rn 4852  df-res 4853  df-ima 4854  df-iota 5381  df-fun 5419  df-fn 5420  df-f 5421  df-f1 5422  df-fo 5423  df-f1o 5424  df-fv 5425  df-ov 6047  df-oprab 6048  df-mpt2 6049  df-1st 6312  df-2nd 6313  df-er 6868  df-en 7073  df-dom 7074  df-sdom 7075  df-pnf 9082  df-mnf 9083  df-xr 9084  df-ltxr 9085  df-le 9086  df-neg 9254  df-z 10243  df-uz 10449  df-fz 11004
  Copyright terms: Public domain W3C validator