Theorem eluzfz1 11614

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

Step	Hyp	Ref	Expression
1		eluzel2 11006	. . 3 |- ( N e. ( ZZ>= ` M ) -> M e. ZZ )
2		uzid 11015	. . 3 |- ( M e. ZZ -> M e. ( ZZ>= ` M ) )
3	1, 2	syl 16	. 2 |- ( N e. ( ZZ>= ` M ) -> M e. ( ZZ>= ` M ) )
4		eluzfz 11604	. 2 |- ( ( M e. ( ZZ>= ` M ) /\ N e. ( ZZ>= ` M ) ) -> M e. ( M ... N ) )
5	3, 4	mpancom 667	1 |- ( N e. ( ZZ>= ` M ) -> M e. ( M ... N ) )

Syntax hints:   -> wi 4   e. wcel 1826   ` cfv 5496  (class class class)co 6196   ZZcz 10781   ZZ>=cuz 11001   ...cfz 11593

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-8 1828  ax-9 1830  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360  ax-sep 4488  ax-nul 4496  ax-pow 4543  ax-pr 4601  ax-un 6491  ax-cnex 9459  ax-resscn 9460  ax-pre-lttri 9477

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-eu 2222  df-mo 2223  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ne 2579  df-nel 2580  df-ral 2737  df-rex 2738  df-rab 2741  df-v 3036  df-sbc 3253  df-csb 3349  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-nul 3712  df-if 3858  df-pw 3929  df-sn 3945  df-pr 3947  df-op 3951  df-uni 4164  df-iun 4245  df-br 4368  df-opab 4426  df-mpt 4427  df-id 4709  df-xp 4919  df-rel 4920  df-cnv 4921  df-co 4922  df-dm 4923  df-rn 4924  df-res 4925  df-ima 4926  df-iota 5460  df-fun 5498  df-fn 5499  df-f 5500  df-f1 5501  df-fo 5502  df-f1o 5503  df-fv 5504  df-ov 6199  df-oprab 6200  df-mpt2 6201  df-1st 6699  df-2nd 6700  df-er 7229  df-en 7436  df-dom 7437  df-sdom 7438  df-pnf 9541  df-mnf 9542  df-xr 9543  df-ltxr 9544  df-le 9545  df-neg 9721  df-z 10782  df-uz 11002  df-fz 11594

This theorem is referenced by:  elfz3  11617  fzn0  11621  fzopth  11642  seqcl  12030  seqfveq  12034  seqshft2  12036  monoord  12040  monoord2  12041  seqcaopr3  12045  seqf1olem2a  12048  seqf1olem2  12050  seqhomo  12057  seqcoll  12416  swrd0val  12557  splid  12640  spllen  12641  splfv1  12642  splfv2a  12643  splval2  12644  fsum1p  13570  telfsumo  13618  telfsumo2  13619  fsumparts  13622  mertenslem2  13696  prodfn0  13705  prodfrec  13706  fprod1p  13774  phicl2  14300  eulerthlem2  14314  4sqlem19  14483  vdwlem1  14501  vdwlem6  14506  vdw  14514  gsumval2  16024  efgsdmi  16867  efgredleme  16878  efgredlemc  16880  efgcpbllemb  16890  frgpuplem  16907  gsumval3OLD  17025  gsumval3  17028  telgsumfzslem  17130  telgsumfzs  17131  pmatcollpw3fi1lem1  19372  chfacfisf  19440  chfacfisfcpmat  19441  cpmadugsumlemF  19462  imasdsf1olem  20961  ovoliunlem1  21998  mbfi1fseqlem3  22209  cxpeq  23218  ppiltx  23568  logexprlim  23617  dchrmusum2  23796  dchrvmasum2lem  23798  mudivsum  23832  mulogsum  23834  mulog2sumlem2  23837  axlowdimlem13  24378  axlowdim1  24383  axlowdim  24385  constr3pthlem3  24778  eupath2  25101  konigsberg  25108  ballotlem4  28620  ballotlemic  28628  ballotlem1c  28629  ballotlem1ri  28656  wrdsplex  28678  subfacp1lem1  28812  subfacp1lem5  28817  subfacp1lem6  28818  cvmliftlem10  28928  cvmliftlem13  28930  inffz  29274  fdc  30404  mettrifi  30416  fmul01lt1lem1  31744  dvnmptdivc  31901  dvnmul  31906  itgspltprt  31944  stoweidlem17  31965  stoweidlem20  31968  stoweidlem34  31982  fourierdlem15  32070  fourierdlem48  32103  fourierdlem50  32105  fourierdlem52  32107  fourierdlem54  32109  fourierdlem64  32119  fourierdlem81  32136  fourierdlem102  32157  fourierdlem103  32158  fourierdlem104  32159  fourierdlem111  32166  fourierdlem114  32169  etransclem10  32193  etransclem14  32197  etransclem15  32198  etransclem24  32207  etransclem35  32218  etransclem44  32227  ssfz12  32651