Theorem eluzfz1 11803

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 11161	. . 3 |- ( N e. ( ZZ>= ` M ) -> M e. ZZ )
2		uzid 11170	. . 3 |- ( M e. ZZ -> M e. ( ZZ>= ` M ) )
3	1, 2	syl 17	. 2 |- ( N e. ( ZZ>= ` M ) -> M e. ( ZZ>= ` M ) )
4		eluzfz 11792	. 2 |- ( ( M e. ( ZZ>= ` M ) /\ N e. ( ZZ>= ` M ) ) -> M e. ( M ... N ) )
5	3, 4	mpancom 674	1 |- ( N e. ( ZZ>= ` M ) -> M e. ( M ... N ) )

Syntax hints:   -> wi 4   e. wcel 1886   ` cfv 5581  (class class class)co 6288   ZZcz 10934   ZZ>=cuz 11156   ...cfz 11781

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-8 1888  ax-9 1895  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-sep 4524  ax-nul 4533  ax-pow 4580  ax-pr 4638  ax-un 6580  ax-cnex 9592  ax-resscn 9593  ax-pre-lttri 9610

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 985  df-3an 986  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-eu 2302  df-mo 2303  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-nel 2624  df-ral 2741  df-rex 2742  df-rab 2745  df-v 3046  df-sbc 3267  df-csb 3363  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-nul 3731  df-if 3881  df-pw 3952  df-sn 3968  df-pr 3970  df-op 3974  df-uni 4198  df-iun 4279  df-br 4402  df-opab 4461  df-mpt 4462  df-id 4748  df-xp 4839  df-rel 4840  df-cnv 4841  df-co 4842  df-dm 4843  df-rn 4844  df-res 4845  df-ima 4846  df-iota 5545  df-fun 5583  df-fn 5584  df-f 5585  df-f1 5586  df-fo 5587  df-f1o 5588  df-fv 5589  df-ov 6291  df-oprab 6292  df-mpt2 6293  df-1st 6790  df-2nd 6791  df-er 7360  df-en 7567  df-dom 7568  df-sdom 7569  df-pnf 9674  df-mnf 9675  df-xr 9676  df-ltxr 9677  df-le 9678  df-neg 9860  df-z 10935  df-uz 11157  df-fz 11782

This theorem is referenced by:  elfz3  11806  fzn0  11810  fzopth  11832  seqcl  12230  seqfveq  12234  seqshft2  12236  monoord  12240  monoord2  12241  seqcaopr3  12245  seqf1olem2a  12248  seqf1olem2  12250  seqhomo  12257  seqcoll  12624  swrd0val  12772  splid  12855  spllen  12856  splfv1  12857  splfv2a  12858  splval2  12859  fsum1p  13807  telfsumo  13855  telfsumo2  13856  fsumparts  13859  mertenslem2  13934  prodfn0  13943  prodfrec  13944  fprod1p  14015  phicl2  14709  eulerthlem2  14723  4sqlem19  14906  vdwlem1  14924  vdwlem6  14929  vdw  14937  fvprmselelfz  14995  prmodvdslcmf  14998  gsumval2  16516  efgsdmi  17375  efgredleme  17386  efgredlemc  17388  efgcpbllemb  17398  frgpuplem  17415  gsumval3  17534  telgsumfzslem  17611  telgsumfzs  17612  pmatcollpw3fi1lem1  19803  chfacfisf  19871  chfacfisfcpmat  19872  cpmadugsumlemF  19893  imasdsf1olem  21381  ovoliunlem1  22448  mbfi1fseqlem3  22668  cxpeq  23690  ppiltx  24097  logexprlim  24146  dchrmusum2  24325  dchrvmasum2lem  24327  mudivsum  24361  mulogsum  24363  mulog2sumlem2  24366  axlowdimlem13  24977  axlowdim1  24982  axlowdim  24984  constr3pthlem3  25378  eupath2  25701  konigsberg  25708  fzto1stfv1  28607  fzto1stinvn  28610  lmatfval  28633  lmat22e11  28637  ballotlem4  29324  ballotlemic  29332  ballotlem1c  29333  ballotlem1ri  29360  ballotlemicOLD  29370  ballotlem1cOLD  29371  ballotlem1riOLD  29398  wrdsplex  29420  subfacp1lem1  29895  subfacp1lem5  29900  subfacp1lem6  29901  cvmliftlem10  30010  cvmliftlem13  30012  inffz  30356  fwddifnp1  30925  poimirlem6  31939  poimirlem7  31940  poimirlem16  31949  poimirlem17  31950  poimirlem19  31952  poimirlem28  31961  fdc  32067  mettrifi  32079  fmul01lt1lem1  37656  dvnmptdivc  37807  dvnmul  37812  itgspltprt  37850  stoweidlem17  37871  stoweidlem20  37874  stoweidlem34  37889  fourierdlem15  37978  fourierdlem48  38012  fourierdlem50  38014  fourierdlem52  38016  fourierdlem54  38018  fourierdlem64  38028  fourierdlem81  38045  fourierdlem102  38066  fourierdlem103  38067  fourierdlem104  38068  fourierdlem111  38075  fourierdlem114  38078  etransclem10  38103  etransclem14  38107  etransclem15  38108  etransclem24  38117  etransclem35  38128  etransclem44  38137  smonoord  38712  ssfz12  39041