Theorem eluzfz2 11571

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

Proof of Theorem eluzfz2

Step	Hyp	Ref	Expression
1		eluzelz 10976	. . 3 |- ( N e. ( ZZ>= ` M ) -> N e. ZZ )
2		uzid 10981	. . 3 |- ( N e. ZZ -> N e. ( ZZ>= ` N ) )
3	1, 2	syl 16	. 2 |- ( N e. ( ZZ>= ` M ) -> N e. ( ZZ>= ` N ) )
4		eluzfz 11560	. 2 |- ( ( N e. ( ZZ>= ` M ) /\ N e. ( ZZ>= ` N ) ) -> N e. ( M ... N ) )
5	3, 4	mpdan 668	1 |- ( N e. ( ZZ>= ` M ) -> N e. ( M ... N ) )

Syntax hints:   -> wi 4   e. wcel 1758   ` cfv 5521  (class class class)co 6195   ZZcz 10752   ZZ>=cuz 10967   ...cfz 11549

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1954  ax-ext 2431  ax-sep 4516  ax-nul 4524  ax-pow 4573  ax-pr 4634  ax-un 6477  ax-cnex 9444  ax-resscn 9445  ax-pre-lttri 9462

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2265  df-mo 2266  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2602  df-ne 2647  df-nel 2648  df-ral 2801  df-rex 2802  df-rab 2805  df-v 3074  df-sbc 3289  df-csb 3391  df-dif 3434  df-un 3436  df-in 3438  df-ss 3445  df-nul 3741  df-if 3895  df-pw 3965  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4195  df-iun 4276  df-br 4396  df-opab 4454  df-mpt 4455  df-id 4739  df-xp 4949  df-rel 4950  df-cnv 4951  df-co 4952  df-dm 4953  df-rn 4954  df-res 4955  df-ima 4956  df-iota 5484  df-fun 5523  df-fn 5524  df-f 5525  df-f1 5526  df-fo 5527  df-f1o 5528  df-fv 5529  df-ov 6198  df-oprab 6199  df-mpt2 6200  df-1st 6682  df-2nd 6683  df-er 7206  df-en 7416  df-dom 7417  df-sdom 7418  df-pnf 9526  df-mnf 9527  df-xr 9528  df-ltxr 9529  df-le 9530  df-neg 9704  df-z 10753  df-uz 10968  df-fz 11550

This theorem is referenced by:  eluzfz2b  11572  fzopth  11607  fzsuc  11614  fseq1p1m1  11646  fzm1  11652  fzneuz  11653  fzoend  11730  uzindi  11915  seqcl2  11936  seqfveq2  11940  seqshft2  11944  monoord  11948  monoord2  11949  seqsplit  11951  seqcaopr3  11953  seqf1olem2a  11956  seqf1olem1  11957  seqf1olem2  11958  seqid2  11964  seqhomo  11965  seqcoll  12329  seqcoll2  12330  swrdid  12434  wrdeqcats1  12481  wrdeqs1cat  12482  swrdccatin12lem2  12493  swrdccatin12lem3  12494  swrdccatin12  12495  swrdccat3b  12500  splid  12508  spllen  12509  splval2  12512  summolem2a  13305  fsumm1  13333  fsumtscopo  13378  fsumtscopo2  13379  fsumparts  13382  sadadd  13776  sadass  13780  smuval2  13791  vdwlem6  14160  efgredleme  16356  efgredlemc  16358  efgcpbllemb  16368  frgpuplem  16385  iscmet3lem1  20929  iscmet3lem2  20930  voliunlem1  21159  volsup  21165  mbfi1fseqlem3  21323  wilthlem2  22535  wilthlem3  22536  chtub  22679  dchrisum0flb  22887  pntpbnd1  22963  pntlemf  22982  spthonepeq  23633  constr3pthlem3  23690  eupap1  23744  konigsberg  23755  ballotlemfc0  27014  ballotlemfcc  27015  ballotlemfrci  27049  gsumnunsn  27076  wrdsplex  27078  cvmliftlem10  27322  supfz  27525  prodfn0  27548  prodfrec  27549  prodmolem2a  27586  fprodm1  27616  volsupnfl  28579  sdclem2  28781  fdc  28784  mettrifi  28796  fmul01lt1lem2  29909  stoweidlem3  29941  stoweidlem11  29949  stoweidlem17  29955  stoweidlem34  29972  ssfz12  30340  elfzubelfz  30344  elfzlble  30351  wwlknext  30499  telescfzgsumlem  30956  telescfzgsum  30957  pmatcollpw3fi1lem1  31254  chfacfisf  31321  chfacfisfcpmat  31322