Theorem eluzfz1 11574

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 10976	. . 3 |- ( N e. ( ZZ>= ` M ) -> M e. ZZ )
2		uzid 10985	. . 3 |- ( M e. ZZ -> M e. ( ZZ>= ` M ) )
3	1, 2	syl 16	. 2 |- ( N e. ( ZZ>= ` M ) -> M e. ( ZZ>= ` M ) )
4		eluzfz 11564	. 2 |- ( ( M e. ( ZZ>= ` M ) /\ N e. ( ZZ>= ` M ) ) -> M e. ( M ... N ) )
5	3, 4	mpancom 669	1 |- ( N e. ( ZZ>= ` M ) -> M e. ( M ... N ) )

Syntax hints:   -> wi 4   e. wcel 1758   ` cfv 5525  (class class class)co 6199   ZZcz 10756   ZZ>=cuz 10971   ...cfz 11553

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 1955  ax-ext 2432  ax-sep 4520  ax-nul 4528  ax-pow 4577  ax-pr 4638  ax-un 6481  ax-cnex 9448  ax-resscn 9449  ax-pre-lttri 9466

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 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2649  df-nel 2650  df-ral 2803  df-rex 2804  df-rab 2807  df-v 3078  df-sbc 3293  df-csb 3395  df-dif 3438  df-un 3440  df-in 3442  df-ss 3449  df-nul 3745  df-if 3899  df-pw 3969  df-sn 3985  df-pr 3987  df-op 3991  df-uni 4199  df-iun 4280  df-br 4400  df-opab 4458  df-mpt 4459  df-id 4743  df-xp 4953  df-rel 4954  df-cnv 4955  df-co 4956  df-dm 4957  df-rn 4958  df-res 4959  df-ima 4960  df-iota 5488  df-fun 5527  df-fn 5528  df-f 5529  df-f1 5530  df-fo 5531  df-f1o 5532  df-fv 5533  df-ov 6202  df-oprab 6203  df-mpt2 6204  df-1st 6686  df-2nd 6687  df-er 7210  df-en 7420  df-dom 7421  df-sdom 7422  df-pnf 9530  df-mnf 9531  df-xr 9532  df-ltxr 9533  df-le 9534  df-neg 9708  df-z 10757  df-uz 10972  df-fz 11554

This theorem is referenced by:  elfz3  11577  fzn0  11580  fzopth  11611  elfzp12  11655  seqcl  11942  seqfveq  11946  seqshft2  11948  monoord  11952  monoord2  11953  seqcaopr3  11957  seqf1olem2a  11960  seqf1olem2  11962  seqhomo  11969  bcn0  12202  seqcoll  12333  swrd0val  12434  swrdid  12438  wrdeqcats1  12485  wrdeqs1cat  12486  splid  12512  spllen  12513  splfv1  12514  splfv2a  12515  splval2  12516  fsum1p  13339  fsumtscopo  13382  fsumtscopo2  13383  fsumparts  13386  mertenslem2  13462  phicl2  13960  eulerthlem2  13974  4sqlem19  14141  vdwlem1  14159  vdwlem6  14164  vdw  14172  gsumval2  15631  efgsdmi  16349  efgredleme  16360  efgredlemc  16362  efgcpbllemb  16372  frgpuplem  16389  gsumval3OLD  16502  gsumval3  16505  imasdsf1olem  20079  ovoliunlem1  21116  mbfi1fseqlem3  21327  cxpeq  22327  ppiltx  22647  logexprlim  22696  dchrmusum2  22875  dchrvmasum2lem  22877  mudivsum  22911  mulogsum  22913  mulog2sumlem2  22916  axlowdimlem13  23351  axlowdim1  23356  axlowdim  23358  spthonepeq  23637  constr3pthlem3  23694  eupath2  23752  konigsberg  23759  ballotlem4  27024  ballotlemic  27032  ballotlem1c  27033  ballotlem1ri  27060  wrdsplex  27082  subfacp1lem1  27210  subfacp1lem5  27215  subfacp1lem6  27216  cvmliftlem10  27326  cvmliftlem13  27328  inffz  27530  prodfn0  27552  prodfrec  27553  fprod1p  27621  fdc  28788  mettrifi  28800  fmul01lt1lem1  29912  stoweidlem17  29959  stoweidlem20  29962  stoweidlem34  29976  ssfz12  30344  telescfzgsumlem  30960  telescfzgsum  30961  pmatcollpw3fi1lem1  31258  chfacfisf  31325  chfacfisfcpmat  31326  cpmadugsumlemF  31347