Theorem elfzuz 13181

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

Syntax hints:   → wi 4   ∈ wcel 2108  ‘cfv 6418  (class class class)co 7255  ℤ_≥cuz 12511  ...cfz 13168

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347  ax-un 7566  ax-cnex 10858  ax-resscn 10859

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-fv 6426  df-ov 7258  df-oprab 7259  df-mpo 7260  df-1st 7804  df-2nd 7805  df-neg 11138  df-z 12250  df-uz 12512  df-fz 13169

This theorem is referenced by:  elfzel1  13184  elfzelz  13185  elfzle1  13188  eluzfz2b  13194  fzsplit2  13210  fzsplit  13211  fzopth  13222  fzss1  13224  fzss2  13225  fzssuz  13226  fzp1elp1  13238  uzsplit  13257  elfzmlbm  13295  predfz  13310  fzosplit  13348  seqf2  13670  seqfeq2  13674  seqfeq  13676  sermono  13683  seqf1olem2  13691  seqz  13699  seqfeq3  13701  ser0  13703  seqcoll  14106  swrdval2  14287  swrdswrd  14346  pfxccatin12  14374  pfxccatpfx2  14378  spllen  14395  swrds2m  14582  limsupgre  15118  clim2ser  15294  clim2ser2  15295  isermulc2  15297  iserle  15299  climub  15301  isercolllem1  15304  isercolllem3  15306  isercoll2  15308  iseraltlem1  15321  fsumcvg  15352  fsumser  15370  isumclim3  15399  isumadd  15407  fsump1i  15409  fsum0diaglem  15416  o1fsum  15453  iserabs  15455  cvgcmp  15456  cvgcmpub  15457  cvgcmpce  15458  isumsplit  15480  isum1p  15481  isumsup2  15486  climcndslem1  15489  climcndslem2  15490  climcnds  15491  geoserg  15506  mertenslem1  15524  clim2div  15529  prodf1  15531  prodfn0  15534  ntrivcvgmullem  15541  fprodcvg  15568  fprodntriv  15580  fprodabs  15612  fprodeq0  15613  iprodclim3  15638  iprodmul  15641  fprodefsum  15732  prmind2  16318  prmdvdsfz  16338  pcfac  16528  prmreclem4  16548  prmreclem5  16549  prmgaplem1  16678  prmgaplem2  16679  prmgaplcmlem2  16681  prmgapprmolem  16690  efgtlen  19247  efgredleme  19264  ovolunlem1a  24565  ovolicc1  24585  uniioombllem3  24654  dvfsumrlimf  25094  dvfsumlem1  25095  dvfsumlem2  25096  dvfsumlem3  25097  dvfsumlem4  25098  dvfsum2  25103  coeidlem  25303  coeid3  25306  vieta1lem2  25376  mtest  25468  mtestbdd  25469  birthdaylem2  26007  wilth  26125  ftalem4  26130  ftalem5  26131  chtub  26265  mersenne  26280  bposlem6  26342  lgsdilem2  26386  rplogsumlem1  26537  rplogsumlem2  26538  dchrisumlem2  26543  dchrisum0lem1  26569  logdivbnd  26609  pntrsumbnd2  26620  pntrlog2bndlem1  26630  pntpbnd1  26639  pntpbnd2  26640  pntlemh  26652  pntlemj  26656  axlowdimlem17  27229  fzsplit3  31017  swrdrn2  31128  swrdrn3  31129  swrdf1  31130  swrdrndisj  31131  ballotlemfrci  32394  subfacp1lem3  33044  knoppcnlem11  34610  poimirlem1  35705  poimirlem2  35706  poimirlem31  35735  poimirlem32  35736  mblfinlem2  35742  mettrifi  35842  geomcau  35844  fzsplitnd  39919  aks4d1p3  40014  iunincfi  42533  elfzfzo  42704  fsumsermpt  43010  fmulcl  43012  fmuldfeqlem1  43013  iblspltprt  43404  itgspltprt  43410  stoweidlem11  43442  stoweidlem17  43448  stirlinglem7  43511  fourierdlem15  43553  fourierdlem25  43563  sge0isum  43855  sge0seq  43874  sge0reuz  43875  sge0reuzb  43876  iundjiun  43888  meaiuninclem  43908  carageniuncllem1  43949  carageniuncllem2  43950  caratheodorylem1  43954  ssfz12  44694  iccpartgt  44767