Theorem elfzuz 13251

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

Syntax hints:   → wi 4   ∈ wcel 2110  ‘cfv 6432  (class class class)co 7271  ℤ_≥cuz 12581  ...cfz 13238

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2711  ax-sep 5227  ax-nul 5234  ax-pr 5356  ax-un 7582  ax-cnex 10928  ax-resscn 10929

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2072  df-mo 2542  df-eu 2571  df-clab 2718  df-cleq 2732  df-clel 2818  df-nfc 2891  df-ral 3071  df-rex 3072  df-rab 3075  df-v 3433  df-sbc 3721  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4846  df-iun 4932  df-br 5080  df-opab 5142  df-mpt 5163  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 6390  df-fun 6434  df-fn 6435  df-f 6436  df-fv 6440  df-ov 7274  df-oprab 7275  df-mpo 7276  df-1st 7824  df-2nd 7825  df-neg 11208  df-z 12320  df-uz 12582  df-fz 13239

This theorem is referenced by:  elfzel1  13254  elfzelz  13255  elfzle1  13258  eluzfz2b  13264  fzsplit2  13280  fzsplit  13281  fzopth  13292  fzss1  13294  fzss2  13295  fzssuz  13296  fzp1elp1  13308  uzsplit  13327  elfzmlbm  13365  predfz  13380  fzosplit  13418  seqf2  13740  seqfeq2  13744  seqfeq  13746  sermono  13753  seqf1olem2  13761  seqz  13769  seqfeq3  13771  ser0  13773  seqcoll  14176  swrdval2  14357  swrdswrd  14416  pfxccatin12  14444  pfxccatpfx2  14448  spllen  14465  swrds2m  14652  limsupgre  15188  clim2ser  15364  clim2ser2  15365  isermulc2  15367  iserle  15369  climub  15371  isercolllem1  15374  isercolllem3  15376  isercoll2  15378  iseraltlem1  15391  fsumcvg  15422  fsumser  15440  isumclim3  15469  isumadd  15477  fsump1i  15479  fsum0diaglem  15486  o1fsum  15523  iserabs  15525  cvgcmp  15526  cvgcmpub  15527  cvgcmpce  15528  isumsplit  15550  isum1p  15551  isumsup2  15556  climcndslem1  15559  climcndslem2  15560  climcnds  15561  geoserg  15576  mertenslem1  15594  clim2div  15599  prodf1  15601  prodfn0  15604  ntrivcvgmullem  15611  fprodcvg  15638  fprodntriv  15650  fprodabs  15682  fprodeq0  15683  iprodclim3  15708  iprodmul  15711  fprodefsum  15802  prmind2  16388  prmdvdsfz  16408  pcfac  16598  prmreclem4  16618  prmreclem5  16619  prmgaplem1  16748  prmgaplem2  16749  prmgaplcmlem2  16751  prmgapprmolem  16760  efgtlen  19330  efgredleme  19347  ovolunlem1a  24658  ovolicc1  24678  uniioombllem3  24747  dvfsumrlimf  25187  dvfsumlem1  25188  dvfsumlem2  25189  dvfsumlem3  25190  dvfsumlem4  25191  dvfsum2  25196  coeidlem  25396  coeid3  25399  vieta1lem2  25469  mtest  25561  mtestbdd  25562  birthdaylem2  26100  wilth  26218  ftalem4  26223  ftalem5  26224  chtub  26358  mersenne  26373  bposlem6  26435  lgsdilem2  26479  rplogsumlem1  26630  rplogsumlem2  26631  dchrisumlem2  26636  dchrisum0lem1  26662  logdivbnd  26702  pntrsumbnd2  26713  pntrlog2bndlem1  26723  pntpbnd1  26732  pntpbnd2  26733  pntlemh  26745  pntlemj  26749  axlowdimlem17  27324  fzsplit3  31111  swrdrn2  31222  swrdrn3  31223  swrdf1  31224  swrdrndisj  31225  ballotlemfrci  32490  subfacp1lem3  33140  knoppcnlem11  34679  poimirlem1  35774  poimirlem2  35775  poimirlem31  35804  poimirlem32  35805  mblfinlem2  35811  mettrifi  35911  geomcau  35913  fzsplitnd  39988  aks4d1p3  40083  iunincfi  42614  elfzfzo  42785  fsumsermpt  43091  fmulcl  43093  fmuldfeqlem1  43094  iblspltprt  43485  itgspltprt  43491  stoweidlem11  43523  stoweidlem17  43529  stirlinglem7  43592  fourierdlem15  43634  fourierdlem25  43644  sge0isum  43936  sge0seq  43955  sge0reuz  43956  sge0reuzb  43957  iundjiun  43969  meaiuninclem  43989  carageniuncllem1  44030  carageniuncllem2  44031  caratheodorylem1  44035  ssfz12  44775  iccpartgt  44848