Theorem elfzuz 13468

Description: A member of a finite set of sequential integers belongs to an upper set of integers. (Contributed by NM, 17-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)

Assertion

Ref	Expression
elfzuz	⊢ (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ (ℤ≥‘𝑀))

Proof of Theorem elfzuz

Step	Hyp	Ref	Expression
1		elfzuzb 13466	. 2 ⊢ (𝐾 ∈ (𝑀...𝑁) ↔ (𝐾 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾)))
2	1	simplbi 496	1 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ (ℤ≥‘𝑀))

Syntax hints:   → wi 4   ∈ wcel 2114  ‘cfv 6493  (class class class)co 7361  ℤ_≥cuz 12782  ...cfz 13455

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-nul 5242  ax-pr 5371  ax-un 7683  ax-cnex 11088  ax-resscn 11089

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-fv 6501  df-ov 7364  df-oprab 7365  df-mpo 7366  df-1st 7936  df-2nd 7937  df-neg 11374  df-z 12519  df-uz 12783  df-fz 13456

This theorem is referenced by:  elfzel1  13471  elfzelz  13472  elfzle1  13475  eluzfz2b  13481  fzsplit2  13497  fzsplit  13498  fzopth  13509  fzss1  13511  fzss2  13512  fzssuz  13513  fzp1elp1  13525  uzsplit  13544  elfzmlbm  13586  predfz  13601  fzosplit  13641  seqf2  13977  seqfeq2  13981  seqfeq  13983  sermono  13990  seqf1olem2  13998  seqz  14006  seqfeq3  14008  ser0  14010  seqcoll  14420  swrdval2  14603  swrdswrd  14661  pfxccatin12  14689  pfxccatpfx2  14693  spllen  14710  swrds2m  14897  limsupgre  15437  clim2ser  15611  clim2ser2  15612  isermulc2  15614  iserle  15616  climub  15618  isercolllem1  15621  isercolllem3  15623  isercoll2  15625  iseraltlem1  15638  fsumcvg  15668  fsumser  15686  isumclim3  15715  isumadd  15723  fsump1i  15725  fsum0diaglem  15732  o1fsum  15770  iserabs  15772  cvgcmp  15773  cvgcmpub  15774  cvgcmpce  15775  isumsplit  15799  isum1p  15800  isumsup2  15805  climcndslem1  15808  climcndslem2  15809  climcnds  15810  geoserg  15825  mertenslem1  15843  clim2div  15848  prodf1  15850  prodfn0  15853  ntrivcvgmullem  15860  fprodcvg  15889  fprodntriv  15901  fprodabs  15933  fprodeq0  15934  iprodclim3  15959  iprodmul  15962  fprodefsum  16054  prmind2  16648  prmdvdsfz  16669  pcfac  16864  prmreclem4  16884  prmreclem5  16885  prmgaplem1  17014  prmgaplem2  17015  prmgaplcmlem2  17017  prmgapprmolem  17026  efgtlen  19695  efgredleme  19712  ovolunlem1a  25476  ovolicc1  25496  uniioombllem3  25565  dvfsumrlimf  26005  dvfsumlem1  26006  dvfsumlem2  26007  dvfsumlem3  26008  dvfsumlem4  26009  dvfsum2  26014  coeidlem  26215  coeid3  26218  vieta1lem2  26291  mtest  26385  mtestbdd  26386  birthdaylem2  26932  wilth  27051  ftalem4  27056  ftalem5  27057  chtub  27192  mersenne  27207  bposlem6  27269  lgsdilem2  27313  rplogsumlem1  27464  rplogsumlem2  27465  dchrisumlem2  27470  dchrisum0lem1  27496  logdivbnd  27536  pntrsumbnd2  27547  pntrlog2bndlem1  27557  pntpbnd1  27566  pntpbnd2  27567  pntlemh  27579  pntlemj  27583  axlowdimlem17  29044  fzsplit3  32884  swrdrn2  33032  swrdrn3  33033  swrdf1  33034  swrdrndisj  33035  ballotlemfrci  34691  subfacp1lem3  35383  knoppcnlem11  36782  poimirlem1  37959  poimirlem2  37960  poimirlem31  37989  poimirlem32  37990  mblfinlem2  37996  mettrifi  38095  geomcau  38097  fzsplitnd  42438  aks4d1p3  42534  iunincfi  45545  elfzfzo  45731  fsumsermpt  46030  fmulcl  46032  fmuldfeqlem1  46033  iblspltprt  46422  itgspltprt  46428  stoweidlem11  46460  stoweidlem17  46466  stirlinglem7  46529  fourierdlem15  46571  fourierdlem25  46581  sge0isum  46876  sge0seq  46895  sge0reuz  46896  sge0reuzb  46897  iundjiun  46909  meaiuninclem  46929  carageniuncllem1  46970  carageniuncllem2  46971  caratheodorylem1  46975  ssfz12  47777  iccpartgt  47902  indprmfz  48108