Theorem elfzuz 13580

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

Syntax hints:   → wi 4   ∈ wcel 2108  ‘cfv 6573  (class class class)co 7448  ℤ_≥cuz 12903  ...cfz 13567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447  ax-un 7770  ax-cnex 11240  ax-resscn 11241

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3or 1088  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-iun 5017  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-fv 6581  df-ov 7451  df-oprab 7452  df-mpo 7453  df-1st 8030  df-2nd 8031  df-neg 11523  df-z 12640  df-uz 12904  df-fz 13568

This theorem is referenced by:  elfzel1  13583  elfzelz  13584  elfzle1  13587  eluzfz2b  13593  fzsplit2  13609  fzsplit  13610  fzopth  13621  fzss1  13623  fzss2  13624  fzssuz  13625  fzp1elp1  13637  uzsplit  13656  elfzmlbm  13695  predfz  13710  fzosplit  13749  seqf2  14072  seqfeq2  14076  seqfeq  14078  sermono  14085  seqf1olem2  14093  seqz  14101  seqfeq3  14103  ser0  14105  seqcoll  14513  swrdval2  14694  swrdswrd  14753  pfxccatin12  14781  pfxccatpfx2  14785  spllen  14802  swrds2m  14990  limsupgre  15527  clim2ser  15703  clim2ser2  15704  isermulc2  15706  iserle  15708  climub  15710  isercolllem1  15713  isercolllem3  15715  isercoll2  15717  iseraltlem1  15730  fsumcvg  15760  fsumser  15778  isumclim3  15807  isumadd  15815  fsump1i  15817  fsum0diaglem  15824  o1fsum  15861  iserabs  15863  cvgcmp  15864  cvgcmpub  15865  cvgcmpce  15866  isumsplit  15888  isum1p  15889  isumsup2  15894  climcndslem1  15897  climcndslem2  15898  climcnds  15899  geoserg  15914  mertenslem1  15932  clim2div  15937  prodf1  15939  prodfn0  15942  ntrivcvgmullem  15949  fprodcvg  15978  fprodntriv  15990  fprodabs  16022  fprodeq0  16023  iprodclim3  16048  iprodmul  16051  fprodefsum  16143  prmind2  16732  prmdvdsfz  16752  pcfac  16946  prmreclem4  16966  prmreclem5  16967  prmgaplem1  17096  prmgaplem2  17097  prmgaplcmlem2  17099  prmgapprmolem  17108  efgtlen  19768  efgredleme  19785  ovolunlem1a  25550  ovolicc1  25570  uniioombllem3  25639  dvfsumrlimf  26085  dvfsumlem1  26086  dvfsumlem2  26087  dvfsumlem2OLD  26088  dvfsumlem3  26089  dvfsumlem4  26090  dvfsum2  26095  coeidlem  26296  coeid3  26299  vieta1lem2  26371  mtest  26465  mtestbdd  26466  birthdaylem2  27013  wilth  27132  ftalem4  27137  ftalem5  27138  chtub  27274  mersenne  27289  bposlem6  27351  lgsdilem2  27395  rplogsumlem1  27546  rplogsumlem2  27547  dchrisumlem2  27552  dchrisum0lem1  27578  logdivbnd  27618  pntrsumbnd2  27629  pntrlog2bndlem1  27639  pntpbnd1  27648  pntpbnd2  27649  pntlemh  27661  pntlemj  27665  axlowdimlem17  28991  fzsplit3  32799  swrdrn2  32921  swrdrn3  32922  swrdf1  32923  swrdrndisj  32924  ballotlemfrci  34492  subfacp1lem3  35150  knoppcnlem11  36469  poimirlem1  37581  poimirlem2  37582  poimirlem31  37611  poimirlem32  37612  mblfinlem2  37618  mettrifi  37717  geomcau  37719  fzsplitnd  41939  aks4d1p3  42035  iunincfi  44996  elfzfzo  45191  fsumsermpt  45500  fmulcl  45502  fmuldfeqlem1  45503  iblspltprt  45894  itgspltprt  45900  stoweidlem11  45932  stoweidlem17  45938  stirlinglem7  46001  fourierdlem15  46043  fourierdlem25  46053  sge0isum  46348  sge0seq  46367  sge0reuz  46368  sge0reuzb  46369  iundjiun  46381  meaiuninclem  46401  carageniuncllem1  46442  carageniuncllem2  46443  caratheodorylem1  46447  ssfz12  47229  iccpartgt  47301