Theorem elfzuz 13497

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

Syntax hints:   → wi 4   ∈ wcel 2107  ‘cfv 6544  (class class class)co 7409  ℤ_≥cuz 12822  ...cfz 13484

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 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428  ax-un 7725  ax-cnex 11166  ax-resscn 11167

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-fv 6552  df-ov 7412  df-oprab 7413  df-mpo 7414  df-1st 7975  df-2nd 7976  df-neg 11447  df-z 12559  df-uz 12823  df-fz 13485

This theorem is referenced by:  elfzel1  13500  elfzelz  13501  elfzle1  13504  eluzfz2b  13510  fzsplit2  13526  fzsplit  13527  fzopth  13538  fzss1  13540  fzss2  13541  fzssuz  13542  fzp1elp1  13554  uzsplit  13573  elfzmlbm  13611  predfz  13626  fzosplit  13665  seqf2  13987  seqfeq2  13991  seqfeq  13993  sermono  14000  seqf1olem2  14008  seqz  14016  seqfeq3  14018  ser0  14020  seqcoll  14425  swrdval2  14596  swrdswrd  14655  pfxccatin12  14683  pfxccatpfx2  14687  spllen  14704  swrds2m  14892  limsupgre  15425  clim2ser  15601  clim2ser2  15602  isermulc2  15604  iserle  15606  climub  15608  isercolllem1  15611  isercolllem3  15613  isercoll2  15615  iseraltlem1  15628  fsumcvg  15658  fsumser  15676  isumclim3  15705  isumadd  15713  fsump1i  15715  fsum0diaglem  15722  o1fsum  15759  iserabs  15761  cvgcmp  15762  cvgcmpub  15763  cvgcmpce  15764  isumsplit  15786  isum1p  15787  isumsup2  15792  climcndslem1  15795  climcndslem2  15796  climcnds  15797  geoserg  15812  mertenslem1  15830  clim2div  15835  prodf1  15837  prodfn0  15840  ntrivcvgmullem  15847  fprodcvg  15874  fprodntriv  15886  fprodabs  15918  fprodeq0  15919  iprodclim3  15944  iprodmul  15947  fprodefsum  16038  prmind2  16622  prmdvdsfz  16642  pcfac  16832  prmreclem4  16852  prmreclem5  16853  prmgaplem1  16982  prmgaplem2  16983  prmgaplcmlem2  16985  prmgapprmolem  16994  efgtlen  19594  efgredleme  19611  ovolunlem1a  25013  ovolicc1  25033  uniioombllem3  25102  dvfsumrlimf  25542  dvfsumlem1  25543  dvfsumlem2  25544  dvfsumlem3  25545  dvfsumlem4  25546  dvfsum2  25551  coeidlem  25751  coeid3  25754  vieta1lem2  25824  mtest  25916  mtestbdd  25917  birthdaylem2  26457  wilth  26575  ftalem4  26580  ftalem5  26581  chtub  26715  mersenne  26730  bposlem6  26792  lgsdilem2  26836  rplogsumlem1  26987  rplogsumlem2  26988  dchrisumlem2  26993  dchrisum0lem1  27019  logdivbnd  27059  pntrsumbnd2  27070  pntrlog2bndlem1  27080  pntpbnd1  27089  pntpbnd2  27090  pntlemh  27102  pntlemj  27106  axlowdimlem17  28247  fzsplit3  32036  swrdrn2  32149  swrdrn3  32150  swrdf1  32151  swrdrndisj  32152  ballotlemfrci  33557  subfacp1lem3  34204  gg-dvfsumlem2  35214  knoppcnlem11  35427  poimirlem1  36537  poimirlem2  36538  poimirlem31  36567  poimirlem32  36568  mblfinlem2  36574  mettrifi  36673  geomcau  36675  fzsplitnd  40896  aks4d1p3  40991  iunincfi  43831  elfzfzo  44034  fsumsermpt  44343  fmulcl  44345  fmuldfeqlem1  44346  iblspltprt  44737  itgspltprt  44743  stoweidlem11  44775  stoweidlem17  44781  stirlinglem7  44844  fourierdlem15  44886  fourierdlem25  44896  sge0isum  45191  sge0seq  45210  sge0reuz  45211  sge0reuzb  45212  iundjiun  45224  meaiuninclem  45244  carageniuncllem1  45285  carageniuncllem2  45286  caratheodorylem1  45290  ssfz12  46070  iccpartgt  46143