Theorem eluzfz2 10061

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 9566	. . 3 |- ( N e. ( ZZ>= ` M ) -> N e. ZZ )
2		uzid 9571	. . 3 |- ( N e. ZZ -> N e. ( ZZ>= ` N ) )
3	1, 2	syl 14	. 2 |- ( N e. ( ZZ>= ` M ) -> N e. ( ZZ>= ` N ) )
4		eluzfz 10049	. 2 |- ( ( N e. ( ZZ>= ` M ) /\ N e. ( ZZ>= ` N ) ) -> N e. ( M ... N ) )
5	3, 4	mpdan 421	1 |- ( N e. ( ZZ>= ` M ) -> N e. ( M ... N ) )

Syntax hints:   -> wi 4   e. wcel 2160   ` cfv 5235  (class class class)co 5895   ZZcz 9282   ZZ>=cuz 9557   ...cfz 10037

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2162  ax-14 2163  ax-ext 2171  ax-sep 4136  ax-pow 4192  ax-pr 4227  ax-un 4451  ax-setind 4554  ax-cnex 7931  ax-resscn 7932  ax-pre-ltirr 7952

This theorem depends on definitions:  df-bi 117  df-3or 981  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-eu 2041  df-mo 2042  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ne 2361  df-nel 2456  df-ral 2473  df-rex 2474  df-rab 2477  df-v 2754  df-sbc 2978  df-dif 3146  df-un 3148  df-in 3150  df-ss 3157  df-pw 3592  df-sn 3613  df-pr 3614  df-op 3616  df-uni 3825  df-br 4019  df-opab 4080  df-mpt 4081  df-id 4311  df-xp 4650  df-rel 4651  df-cnv 4652  df-co 4653  df-dm 4654  df-rn 4655  df-res 4656  df-ima 4657  df-iota 5196  df-fun 5237  df-fn 5238  df-f 5239  df-fv 5243  df-ov 5898  df-oprab 5899  df-mpo 5900  df-pnf 8023  df-mnf 8024  df-xr 8025  df-ltxr 8026  df-le 8027  df-neg 8160  df-z 9283  df-uz 9558  df-fz 10038

This theorem is referenced by:  eluzfz2b  10062  elfzubelfz  10065  fzopth  10090  fzsuc  10098  fseq1p1m1  10123  fzm1  10129  fzneuz  10130  fzoend  10251  exfzdc  10269  uzsinds  10472  seq3clss  10497  seq3fveq2  10499  seq3shft2  10503  monoord  10506  monoord2  10507  seq3split  10509  seq3caopr3  10511  seq3f1olemp  10532  seq3id3  10537  seq3id2  10539  ser3ge0  10547  seq3coll  10853  summodclem2a  11420  fsumm1  11455  telfsumo  11505  telfsumo2  11506  fsumparts  11509  prodfap0  11584  prodfrecap  11585  prodmodclem2a  11615  fprodm1  11637  eulerthlemrprm  12260  eulerthlema  12261  nninfdclemlt  12501  supfz  15273