Theorem elfzuz 13481

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

Syntax hints:   → wi 4   ∈ wcel 2109  ‘cfv 6511  (class class class)co 7387  ℤ_≥cuz 12793  ...cfz 13468

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387  ax-un 7711  ax-cnex 11124  ax-resscn 11125

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-fv 6519  df-ov 7390  df-oprab 7391  df-mpo 7392  df-1st 7968  df-2nd 7969  df-neg 11408  df-z 12530  df-uz 12794  df-fz 13469

This theorem is referenced by:  elfzel1  13484  elfzelz  13485  elfzle1  13488  eluzfz2b  13494  fzsplit2  13510  fzsplit  13511  fzopth  13522  fzss1  13524  fzss2  13525  fzssuz  13526  fzp1elp1  13538  uzsplit  13557  elfzmlbm  13599  predfz  13614  fzosplit  13653  seqf2  13986  seqfeq2  13990  seqfeq  13992  sermono  13999  seqf1olem2  14007  seqz  14015  seqfeq3  14017  ser0  14019  seqcoll  14429  swrdval2  14611  swrdswrd  14670  pfxccatin12  14698  pfxccatpfx2  14702  spllen  14719  swrds2m  14907  limsupgre  15447  clim2ser  15621  clim2ser2  15622  isermulc2  15624  iserle  15626  climub  15628  isercolllem1  15631  isercolllem3  15633  isercoll2  15635  iseraltlem1  15648  fsumcvg  15678  fsumser  15696  isumclim3  15725  isumadd  15733  fsump1i  15735  fsum0diaglem  15742  o1fsum  15779  iserabs  15781  cvgcmp  15782  cvgcmpub  15783  cvgcmpce  15784  isumsplit  15806  isum1p  15807  isumsup2  15812  climcndslem1  15815  climcndslem2  15816  climcnds  15817  geoserg  15832  mertenslem1  15850  clim2div  15855  prodf1  15857  prodfn0  15860  ntrivcvgmullem  15867  fprodcvg  15896  fprodntriv  15908  fprodabs  15940  fprodeq0  15941  iprodclim3  15966  iprodmul  15969  fprodefsum  16061  prmind2  16655  prmdvdsfz  16675  pcfac  16870  prmreclem4  16890  prmreclem5  16891  prmgaplem1  17020  prmgaplem2  17021  prmgaplcmlem2  17023  prmgapprmolem  17032  efgtlen  19656  efgredleme  19673  ovolunlem1a  25397  ovolicc1  25417  uniioombllem3  25486  dvfsumrlimf  25931  dvfsumlem1  25932  dvfsumlem2  25933  dvfsumlem2OLD  25934  dvfsumlem3  25935  dvfsumlem4  25936  dvfsum2  25941  coeidlem  26142  coeid3  26145  vieta1lem2  26219  mtest  26313  mtestbdd  26314  birthdaylem2  26862  wilth  26981  ftalem4  26986  ftalem5  26987  chtub  27123  mersenne  27138  bposlem6  27200  lgsdilem2  27244  rplogsumlem1  27395  rplogsumlem2  27396  dchrisumlem2  27401  dchrisum0lem1  27427  logdivbnd  27467  pntrsumbnd2  27478  pntrlog2bndlem1  27488  pntpbnd1  27497  pntpbnd2  27498  pntlemh  27510  pntlemj  27514  axlowdimlem17  28885  fzsplit3  32716  swrdrn2  32876  swrdrn3  32877  swrdf1  32878  swrdrndisj  32879  ballotlemfrci  34519  subfacp1lem3  35169  knoppcnlem11  36491  poimirlem1  37615  poimirlem2  37616  poimirlem31  37645  poimirlem32  37646  mblfinlem2  37652  mettrifi  37751  geomcau  37753  fzsplitnd  41970  aks4d1p3  42066  iunincfi  45088  elfzfzo  45275  fsumsermpt  45577  fmulcl  45579  fmuldfeqlem1  45580  iblspltprt  45971  itgspltprt  45977  stoweidlem11  46009  stoweidlem17  46015  stirlinglem7  46078  fourierdlem15  46120  fourierdlem25  46130  sge0isum  46425  sge0seq  46444  sge0reuz  46445  sge0reuzb  46446  iundjiun  46458  meaiuninclem  46478  carageniuncllem1  46519  carageniuncllem2  46520  caratheodorylem1  46524  ssfz12  47315  iccpartgt  47428