Theorem elfzuz 13494

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

Syntax hints:   → wi 4   ∈ wcel 2098  ‘cfv 6533  (class class class)co 7401  ℤ_≥cuz 12819  ...cfz 13481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-sep 5289  ax-nul 5296  ax-pr 5417  ax-un 7718  ax-cnex 11162  ax-resscn 11163

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ral 3054  df-rex 3063  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-iun 4989  df-br 5139  df-opab 5201  df-mpt 5222  df-id 5564  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-fv 6541  df-ov 7404  df-oprab 7405  df-mpo 7406  df-1st 7968  df-2nd 7969  df-neg 11444  df-z 12556  df-uz 12820  df-fz 13482

This theorem is referenced by:  elfzel1  13497  elfzelz  13498  elfzle1  13501  eluzfz2b  13507  fzsplit2  13523  fzsplit  13524  fzopth  13535  fzss1  13537  fzss2  13538  fzssuz  13539  fzp1elp1  13551  uzsplit  13570  elfzmlbm  13608  predfz  13623  fzosplit  13662  seqf2  13984  seqfeq2  13988  seqfeq  13990  sermono  13997  seqf1olem2  14005  seqz  14013  seqfeq3  14015  ser0  14017  seqcoll  14422  swrdval2  14593  swrdswrd  14652  pfxccatin12  14680  pfxccatpfx2  14684  spllen  14701  swrds2m  14889  limsupgre  15422  clim2ser  15598  clim2ser2  15599  isermulc2  15601  iserle  15603  climub  15605  isercolllem1  15608  isercolllem3  15610  isercoll2  15612  iseraltlem1  15625  fsumcvg  15655  fsumser  15673  isumclim3  15702  isumadd  15710  fsump1i  15712  fsum0diaglem  15719  o1fsum  15756  iserabs  15758  cvgcmp  15759  cvgcmpub  15760  cvgcmpce  15761  isumsplit  15783  isum1p  15784  isumsup2  15789  climcndslem1  15792  climcndslem2  15793  climcnds  15794  geoserg  15809  mertenslem1  15827  clim2div  15832  prodf1  15834  prodfn0  15837  ntrivcvgmullem  15844  fprodcvg  15871  fprodntriv  15883  fprodabs  15915  fprodeq0  15916  iprodclim3  15941  iprodmul  15944  fprodefsum  16035  prmind2  16619  prmdvdsfz  16639  pcfac  16831  prmreclem4  16851  prmreclem5  16852  prmgaplem1  16981  prmgaplem2  16982  prmgaplcmlem2  16984  prmgapprmolem  16993  efgtlen  19636  efgredleme  19653  ovolunlem1a  25347  ovolicc1  25367  uniioombllem3  25436  dvfsumrlimf  25881  dvfsumlem1  25882  dvfsumlem2  25883  dvfsumlem2OLD  25884  dvfsumlem3  25885  dvfsumlem4  25886  dvfsum2  25891  coeidlem  26091  coeid3  26094  vieta1lem2  26165  mtest  26257  mtestbdd  26258  birthdaylem2  26800  wilth  26919  ftalem4  26924  ftalem5  26925  chtub  27061  mersenne  27076  bposlem6  27138  lgsdilem2  27182  rplogsumlem1  27333  rplogsumlem2  27334  dchrisumlem2  27339  dchrisum0lem1  27365  logdivbnd  27405  pntrsumbnd2  27416  pntrlog2bndlem1  27426  pntpbnd1  27435  pntpbnd2  27436  pntlemh  27448  pntlemj  27452  axlowdimlem17  28685  fzsplit3  32474  swrdrn2  32585  swrdrn3  32586  swrdf1  32587  swrdrndisj  32588  ballotlemfrci  34015  subfacp1lem3  34662  knoppcnlem11  35869  poimirlem1  36979  poimirlem2  36980  poimirlem31  37009  poimirlem32  37010  mblfinlem2  37016  mettrifi  37115  geomcau  37117  fzsplitnd  41341  aks4d1p3  41436  iunincfi  44271  elfzfzo  44471  fsumsermpt  44780  fmulcl  44782  fmuldfeqlem1  44783  iblspltprt  45174  itgspltprt  45180  stoweidlem11  45212  stoweidlem17  45218  stirlinglem7  45281  fourierdlem15  45323  fourierdlem25  45333  sge0isum  45628  sge0seq  45647  sge0reuz  45648  sge0reuzb  45649  iundjiun  45661  meaiuninclem  45681  carageniuncllem1  45722  carageniuncllem2  45723  caratheodorylem1  45727  ssfz12  46507  iccpartgt  46580