Theorem eluzfz1 13664

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	⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ (𝑀...𝑁))

Proof of Theorem eluzfz1

Step	Hyp	Ref	Expression
1		eluzel2 12970	. . 3 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ)
2		uzid 12980	. . 3 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ≥‘𝑀))
3	1, 2	syl 18	. 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ (ℤ≥‘𝑀))
4		eluzfz 13651	. 2 ⊢ ((𝑀 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝑀)) → 𝑀 ∈ (𝑀...𝑁))
5	3, 4	mpancom 701	1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ (𝑀...𝑁))

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  ‘cfv 6538  (class class class)co 7420  ℤcz 12693  ℤ_≥cuz 12965  ...cfz 13639

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7751  ax-cnex 11256  ax-resscn 11257  ax-pre-lttri 11274

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5545  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-ov 7423  df-oprab 7424  df-mpo 7425  df-1st 8001  df-2nd 8002  df-er 8717  df-en 8974  df-dom 8975  df-sdom 8976  df-pnf 11345  df-mnf 11346  df-xr 11347  df-ltxr 11348  df-le 11349  df-neg 11544  df-z 12694  df-uz 12966  df-fz 13640

This theorem is used by:  elfz3  13667  fzn0  13671  fzopth  13695  seqcl  14165  seqfveq  14169  seqshft2  14171  monoord  14175  monoord2  14176  seqcaopr3  14180  seqf1olem2a  14183  seqf1olem2  14185  seqhomo  14192  seqcoll  14609  fsum1p  15919  telfsumo  15969  telfsumo2  15970  fsumparts  15973  mertenslem2  16054  prodfn0  16063  prodfrec  16064  fprod1p  16135  phicl2  16945  eulerthlem2  16959  4sqlem19  17141  vdwlem1  17159  vdwlem6  17164  vdw  17172  fvprmselelfz  17222  prmodvdslcmf  17225  gsumval2  18875  gsumsplit1r  18876  efgsdmi  19946  gsumval3  20121  telgsumfzslem  20202  telgsumfzs  20203  pmatcollpw3fi1lem1  23104  chfacfisf  23172  chfacfisfcpmat  23173  cpmadugsumlemF  23194  imasdsf1olem  24692  ovoliunlem1  25823  mbfi1fseqlem3  26038  cxpeq  27085  ppiltx  27504  logexprlim  27552  dchrmusum2  27821  dchrvmasum2lem  27823  mudivsum  27857  mulogsum  27859  mulog2sumlem2  27862  axlowdimlem13  29532  axlowdim1  29537  axlowdim  29539  crctcshwlkn0lem6  30404  gsummptfzsplitla  33620  fzto1stfv1  33662  fzto1stinvn  33665  cycpmco2f1  33685  lmatfval  34446  lmat22e11  34450  ballotlem4  35131  ballotlemic  35139  ballotlem1c  35140  ballotlem1ri  35167  subfacp1lem1  35944  subfacp1lem5  35949  subfacp1lem6  35950  cvmliftlem10  36059  cvmliftlem13  36061  inffz  36495  fwddifnp1  36930  poimirlem6  38545  poimirlem7  38546  poimirlem16  38555  poimirlem17  38556  poimirlem19  38558  poimirlem28  38567  fdc  38680  mettrifi  38692  sticksstones12a  43208  monoordxrv  46491  monoord2xrv  46493  fmul01lt1lem1  46596  dvnmptdivc  46948  dvnmul  46953  itgspltprt  46989  stoweidlem17  47027  stoweidlem20  47030  stoweidlem34  47044  fourierdlem15  47132  fourierdlem48  47164  fourierdlem50  47166  fourierdlem52  47168  fourierdlem54  47170  fourierdlem64  47180  fourierdlem81  47197  fourierdlem102  47218  fourierdlem103  47219  fourierdlem104  47220  fourierdlem111  47227  fourierdlem114  47230  etransclem10  47254  etransclem14  47258  etransclem15  47259  etransclem24  47268  etransclem35  47279  etransclem44  47288  smfmullem4  47804  ssfz12  48384  smonoord  48447  gpg5grlim  49191  gpg5grlic  49192