Theorem elfzuz 13261

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 13259	. 2 ⊢ (𝐾 ∈ (𝑀...𝑁) ↔ (𝐾 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝐾)))
2	1	simplbi 498	1 ⊢ (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ (ℤ≥‘𝑀))

Syntax hints:   → wi 4   ∈ wcel 2107  ‘cfv 6437  (class class class)co 7284  ℤ_≥cuz 12591  ...cfz 13248

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-sep 5224  ax-nul 5231  ax-pr 5353  ax-un 7597  ax-cnex 10936  ax-resscn 10937

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3435  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-pw 4536  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-iun 4927  df-br 5076  df-opab 5138  df-mpt 5159  df-id 5490  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-iota 6395  df-fun 6439  df-fn 6440  df-f 6441  df-fv 6445  df-ov 7287  df-oprab 7288  df-mpo 7289  df-1st 7840  df-2nd 7841  df-neg 11217  df-z 12329  df-uz 12592  df-fz 13249

This theorem is referenced by:  elfzel1  13264  elfzelz  13265  elfzle1  13268  eluzfz2b  13274  fzsplit2  13290  fzsplit  13291  fzopth  13302  fzss1  13304  fzss2  13305  fzssuz  13306  fzp1elp1  13318  uzsplit  13337  elfzmlbm  13375  predfz  13390  fzosplit  13429  seqf2  13751  seqfeq2  13755  seqfeq  13757  sermono  13764  seqf1olem2  13772  seqz  13780  seqfeq3  13782  ser0  13784  seqcoll  14187  swrdval2  14368  swrdswrd  14427  pfxccatin12  14455  pfxccatpfx2  14459  spllen  14476  swrds2m  14663  limsupgre  15199  clim2ser  15375  clim2ser2  15376  isermulc2  15378  iserle  15380  climub  15382  isercolllem1  15385  isercolllem3  15387  isercoll2  15389  iseraltlem1  15402  fsumcvg  15433  fsumser  15451  isumclim3  15480  isumadd  15488  fsump1i  15490  fsum0diaglem  15497  o1fsum  15534  iserabs  15536  cvgcmp  15537  cvgcmpub  15538  cvgcmpce  15539  isumsplit  15561  isum1p  15562  isumsup2  15567  climcndslem1  15570  climcndslem2  15571  climcnds  15572  geoserg  15587  mertenslem1  15605  clim2div  15610  prodf1  15612  prodfn0  15615  ntrivcvgmullem  15622  fprodcvg  15649  fprodntriv  15661  fprodabs  15693  fprodeq0  15694  iprodclim3  15719  iprodmul  15722  fprodefsum  15813  prmind2  16399  prmdvdsfz  16419  pcfac  16609  prmreclem4  16629  prmreclem5  16630  prmgaplem1  16759  prmgaplem2  16760  prmgaplcmlem2  16762  prmgapprmolem  16771  efgtlen  19341  efgredleme  19358  ovolunlem1a  24669  ovolicc1  24689  uniioombllem3  24758  dvfsumrlimf  25198  dvfsumlem1  25199  dvfsumlem2  25200  dvfsumlem3  25201  dvfsumlem4  25202  dvfsum2  25207  coeidlem  25407  coeid3  25410  vieta1lem2  25480  mtest  25572  mtestbdd  25573  birthdaylem2  26111  wilth  26229  ftalem4  26234  ftalem5  26235  chtub  26369  mersenne  26384  bposlem6  26446  lgsdilem2  26490  rplogsumlem1  26641  rplogsumlem2  26642  dchrisumlem2  26647  dchrisum0lem1  26673  logdivbnd  26713  pntrsumbnd2  26724  pntrlog2bndlem1  26734  pntpbnd1  26743  pntpbnd2  26744  pntlemh  26756  pntlemj  26760  axlowdimlem17  27335  fzsplit3  31124  swrdrn2  31235  swrdrn3  31236  swrdf1  31237  swrdrndisj  31238  ballotlemfrci  32503  subfacp1lem3  33153  knoppcnlem11  34692  poimirlem1  35787  poimirlem2  35788  poimirlem31  35817  poimirlem32  35818  mblfinlem2  35824  mettrifi  35924  geomcau  35926  fzsplitnd  39998  aks4d1p3  40093  iunincfi  42651  elfzfzo  42822  fsumsermpt  43127  fmulcl  43129  fmuldfeqlem1  43130  iblspltprt  43521  itgspltprt  43527  stoweidlem11  43559  stoweidlem17  43565  stirlinglem7  43628  fourierdlem15  43670  fourierdlem25  43680  sge0isum  43972  sge0seq  43991  sge0reuz  43992  sge0reuzb  43993  iundjiun  44005  meaiuninclem  44025  carageniuncllem1  44066  carageniuncllem2  44067  caratheodorylem1  44071  ssfz12  44817  iccpartgt  44890