Theorem elfzuz 13496

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

Syntax hints:   → wi 4   ∈ wcel 2106  ‘cfv 6543  (class class class)co 7408  ℤ_≥cuz 12821  ...cfz 13483

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427  ax-un 7724  ax-cnex 11165  ax-resscn 11166

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-fv 6551  df-ov 7411  df-oprab 7412  df-mpo 7413  df-1st 7974  df-2nd 7975  df-neg 11446  df-z 12558  df-uz 12822  df-fz 13484

This theorem is referenced by:  elfzel1  13499  elfzelz  13500  elfzle1  13503  eluzfz2b  13509  fzsplit2  13525  fzsplit  13526  fzopth  13537  fzss1  13539  fzss2  13540  fzssuz  13541  fzp1elp1  13553  uzsplit  13572  elfzmlbm  13610  predfz  13625  fzosplit  13664  seqf2  13986  seqfeq2  13990  seqfeq  13992  sermono  13999  seqf1olem2  14007  seqz  14015  seqfeq3  14017  ser0  14019  seqcoll  14424  swrdval2  14595  swrdswrd  14654  pfxccatin12  14682  pfxccatpfx2  14686  spllen  14703  swrds2m  14891  limsupgre  15424  clim2ser  15600  clim2ser2  15601  isermulc2  15603  iserle  15605  climub  15607  isercolllem1  15610  isercolllem3  15612  isercoll2  15614  iseraltlem1  15627  fsumcvg  15657  fsumser  15675  isumclim3  15704  isumadd  15712  fsump1i  15714  fsum0diaglem  15721  o1fsum  15758  iserabs  15760  cvgcmp  15761  cvgcmpub  15762  cvgcmpce  15763  isumsplit  15785  isum1p  15786  isumsup2  15791  climcndslem1  15794  climcndslem2  15795  climcnds  15796  geoserg  15811  mertenslem1  15829  clim2div  15834  prodf1  15836  prodfn0  15839  ntrivcvgmullem  15846  fprodcvg  15873  fprodntriv  15885  fprodabs  15917  fprodeq0  15918  iprodclim3  15943  iprodmul  15946  fprodefsum  16037  prmind2  16621  prmdvdsfz  16641  pcfac  16831  prmreclem4  16851  prmreclem5  16852  prmgaplem1  16981  prmgaplem2  16982  prmgaplcmlem2  16984  prmgapprmolem  16993  efgtlen  19593  efgredleme  19610  ovolunlem1a  25012  ovolicc1  25032  uniioombllem3  25101  dvfsumrlimf  25541  dvfsumlem1  25542  dvfsumlem2  25543  dvfsumlem3  25544  dvfsumlem4  25545  dvfsum2  25550  coeidlem  25750  coeid3  25753  vieta1lem2  25823  mtest  25915  mtestbdd  25916  birthdaylem2  26454  wilth  26572  ftalem4  26577  ftalem5  26578  chtub  26712  mersenne  26727  bposlem6  26789  lgsdilem2  26833  rplogsumlem1  26984  rplogsumlem2  26985  dchrisumlem2  26990  dchrisum0lem1  27016  logdivbnd  27056  pntrsumbnd2  27067  pntrlog2bndlem1  27077  pntpbnd1  27086  pntpbnd2  27087  pntlemh  27099  pntlemj  27103  axlowdimlem17  28213  fzsplit3  32000  swrdrn2  32113  swrdrn3  32114  swrdf1  32115  swrdrndisj  32116  ballotlemfrci  33521  subfacp1lem3  34168  gg-dvfsumlem2  35178  knoppcnlem11  35374  poimirlem1  36484  poimirlem2  36485  poimirlem31  36514  poimirlem32  36515  mblfinlem2  36521  mettrifi  36620  geomcau  36622  fzsplitnd  40843  aks4d1p3  40938  iunincfi  43773  elfzfzo  43976  fsumsermpt  44285  fmulcl  44287  fmuldfeqlem1  44288  iblspltprt  44679  itgspltprt  44685  stoweidlem11  44717  stoweidlem17  44723  stirlinglem7  44786  fourierdlem15  44828  fourierdlem25  44838  sge0isum  45133  sge0seq  45152  sge0reuz  45153  sge0reuzb  45154  iundjiun  45166  meaiuninclem  45186  carageniuncllem1  45227  carageniuncllem2  45228  caratheodorylem1  45232  ssfz12  46012  iccpartgt  46085