Theorem eluzfz2 11807

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 11168	. . 3 |- ( N e. ( ZZ>= ` M ) -> N e. ZZ )
2		uzid 11173	. . 3 |- ( N e. ZZ -> N e. ( ZZ>= ` N ) )
3	1, 2	syl 17	. 2 |- ( N e. ( ZZ>= ` M ) -> N e. ( ZZ>= ` N ) )
4		eluzfz 11795	. 2 |- ( ( N e. ( ZZ>= ` M ) /\ N e. ( ZZ>= ` N ) ) -> N e. ( M ... N ) )
5	3, 4	mpdan 674	1 |- ( N e. ( ZZ>= ` M ) -> N e. ( M ... N ) )

Syntax hints:   -> wi 4   e. wcel 1887   ` cfv 5582  (class class class)co 6290   ZZcz 10937   ZZ>=cuz 11159   ...cfz 11784

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-8 1889  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-sep 4525  ax-nul 4534  ax-pow 4581  ax-pr 4639  ax-un 6583  ax-cnex 9595  ax-resscn 9596  ax-pre-lttri 9613

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 986  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-nel 2625  df-ral 2742  df-rex 2743  df-rab 2746  df-v 3047  df-sbc 3268  df-csb 3364  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-nul 3732  df-if 3882  df-pw 3953  df-sn 3969  df-pr 3971  df-op 3975  df-uni 4199  df-iun 4280  df-br 4403  df-opab 4462  df-mpt 4463  df-id 4749  df-xp 4840  df-rel 4841  df-cnv 4842  df-co 4843  df-dm 4844  df-rn 4845  df-res 4846  df-ima 4847  df-iota 5546  df-fun 5584  df-fn 5585  df-f 5586  df-f1 5587  df-fo 5588  df-f1o 5589  df-fv 5590  df-ov 6293  df-oprab 6294  df-mpt2 6295  df-1st 6793  df-2nd 6794  df-er 7363  df-en 7570  df-dom 7571  df-sdom 7572  df-pnf 9677  df-mnf 9678  df-xr 9679  df-ltxr 9680  df-le 9681  df-neg 9863  df-z 10938  df-uz 11160  df-fz 11785

This theorem is referenced by:  eluzfz2b  11808  elfzubelfz  11811  fzopth  11835  fzsuc  11843  fseq1p1m1  11868  fzm1  11874  fzneuz  11875  fzoend  12002  uzindi  12194  seqcl2  12231  seqfveq2  12235  seqshft2  12239  monoord  12243  monoord2  12244  seqsplit  12246  seqcaopr3  12248  seqf1olem2a  12251  seqf1olem1  12252  seqf1olem2  12253  seqid2  12259  seqhomo  12260  seqcoll  12627  seqcoll2  12628  wrdeqs1cat  12831  swrdccatin12lem2  12845  swrdccatin12lem3  12846  swrdccatin12  12847  splid  12860  spllen  12861  splval2  12864  summolem2a  13781  fsumm1  13812  telfsumo  13862  telfsumo2  13863  fsumparts  13866  prodfn0  13950  prodfrec  13951  prodmolem2a  13988  fprodm1  14021  sadadd  14441  sadass  14445  smuval2  14456  vdwlem6  14936  efgredleme  17393  efgredlemc  17395  efgcpbllemb  17405  frgpuplem  17422  telgsumfzslem  17618  telgsumfzs  17619  pmatcollpw3fi1lem1  19810  chfacfisf  19878  chfacfisfcpmat  19879  iscmet3lem1  22261  iscmet3lem2  22262  voliunlem1  22503  volsup  22509  mbfi1fseqlem3  22675  wilthlem2  23994  wilthlem3  23995  chtub  24140  dchrisum0flb  24348  pntpbnd1  24424  pntlemf  24443  spthonepeq  25317  constr3pthlem3  25385  wwlknext  25452  eupap1  25704  konigsberg  25715  submatres  28632  madjusmdetlem1  28653  madjusmdetlem2  28654  madjusmdetlem3  28655  madjusmdetlem4  28656  ballotlemfc0  29325  ballotlemfcc  29326  ballotlemfrci  29360  ballotlemfrciOLD  29398  gsumnunsn  29425  wrdsplex  29427  cvmliftlem10  30017  supfz  30362  fwddifnp1  30932  poimirlem3  31943  poimirlem4  31944  poimirlem16  31956  poimirlem19  31959  poimirlem20  31960  poimirlem23  31963  poimirlem31  31971  volsupnfl  31985  sdclem2  32071  fdc  32074  mettrifi  32086  fmul01lt1lem2  37663  dvnmul  37818  dvnprodlem3  37823  stoweidlem3  37863  stoweidlem11  37871  stoweidlem17  37877  stoweidlem34  37895  fourierdlem15  37984  fourierdlem25  37994  fourierdlem50  38020  fourierdlem52  38022  fourierdlem54  38024  fourierdlem65  38035  fourierdlem81  38051  fourierdlem92  38062  fourierdlem102  38072  fourierdlem111  38081  fourierdlem113  38083  fourierdlem114  38084  etransclem35  38134  sge0p1  38256  carageniuncllem1  38342  caratheodorylem1  38347  smonoord  38718  pfxccatin12lem2  38965  pfxccatin12  38966  ssfz12  39054  elfzlble  39060