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  28216  fzsplit3  32005  swrdrn2  32118  swrdrn3  32119  swrdf1  32120  swrdrndisj  32121  ballotlemfrci  33526  subfacp1lem3  34173  gg-dvfsumlem2  35183  knoppcnlem11  35379  poimirlem1  36489  poimirlem2  36490  poimirlem31  36519  poimirlem32  36520  mblfinlem2  36526  mettrifi  36625  geomcau  36627  fzsplitnd  40848  aks4d1p3  40943  iunincfi  43783  elfzfzo  43986  fsumsermpt  44295  fmulcl  44297  fmuldfeqlem1  44298  iblspltprt  44689  itgspltprt  44695  stoweidlem11  44727  stoweidlem17  44733  stirlinglem7  44796  fourierdlem15  44838  fourierdlem25  44848  sge0isum  45143  sge0seq  45162  sge0reuz  45163  sge0reuzb  45164  iundjiun  45176  meaiuninclem  45196  carageniuncllem1  45237  carageniuncllem2  45238  caratheodorylem1  45242  ssfz12  46022  iccpartgt  46095