Theorem elfzuz 12907

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

Syntax hints:   → wi 4   ∈ wcel 2114  ‘cfv 6357  (class class class)co 7158  ℤ_≥cuz 12246  ...cfz 12895

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pow 5268  ax-pr 5332  ax-un 7463  ax-cnex 10595  ax-resscn 10596

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ne 3019  df-ral 3145  df-rex 3146  df-rab 3149  df-v 3498  df-sbc 3775  df-csb 3886  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-pw 4543  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4841  df-iun 4923  df-br 5069  df-opab 5131  df-mpt 5149  df-id 5462  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-rn 5568  df-res 5569  df-ima 5570  df-iota 6316  df-fun 6359  df-fn 6360  df-f 6361  df-fv 6365  df-ov 7161  df-oprab 7162  df-mpo 7163  df-1st 7691  df-2nd 7692  df-neg 10875  df-z 11985  df-uz 12247  df-fz 12896

This theorem is referenced by:  elfzel1  12910  elfzelz  12911  elfzle1  12913  eluzfz2b  12919  fzsplit2  12935  fzsplit  12936  fzopth  12947  fzss1  12949  fzss2  12950  fzssuz  12951  fzp1elp1  12963  uzsplit  12982  elfzmlbm  13020  predfz  13035  fzosplit  13073  seqf2  13392  seqfeq2  13396  seqfeq  13398  sermono  13405  seqf1olem2  13413  seqz  13421  seqfeq3  13423  ser0  13425  seqcoll  13825  swrdval2  14010  swrdswrd  14069  pfxccatin12  14097  pfxccatpfx2  14101  spllen  14118  swrds2m  14305  limsupgre  14840  clim2ser  15013  clim2ser2  15014  isermulc2  15016  iserle  15018  climub  15020  isercolllem1  15023  isercolllem3  15025  isercoll2  15027  iseraltlem1  15040  fsumcvg  15071  fsumser  15089  isumclim3  15116  isumadd  15124  fsump1i  15126  fsum0diaglem  15133  o1fsum  15170  iserabs  15172  cvgcmp  15173  cvgcmpub  15174  cvgcmpce  15175  isumsplit  15197  isum1p  15198  isumsup2  15203  climcndslem1  15206  climcndslem2  15207  climcnds  15208  geoserg  15223  mertenslem1  15242  clim2div  15247  prodf1  15249  prodfn0  15252  ntrivcvgmullem  15259  fprodcvg  15286  fprodntriv  15298  fprodabs  15330  fprodeq0  15331  iprodclim3  15356  iprodmul  15359  fprodefsum  15450  prmind2  16031  prmdvdsfz  16051  pcfac  16237  prmreclem4  16257  prmreclem5  16258  prmgaplem1  16387  prmgaplem2  16388  prmgaplcmlem2  16390  prmgapprmolem  16399  efgtlen  18854  efgredleme  18871  ovolunlem1a  24099  ovolicc1  24119  uniioombllem3  24188  dvfsumrlimf  24624  dvfsumlem1  24625  dvfsumlem2  24626  dvfsumlem3  24627  dvfsumlem4  24628  dvfsum2  24633  coeidlem  24829  coeid3  24832  vieta1lem2  24902  mtest  24994  mtestbdd  24995  birthdaylem2  25532  wilth  25650  ftalem4  25655  ftalem5  25656  chtub  25790  mersenne  25805  bposlem6  25867  lgsdilem2  25911  rplogsumlem1  26062  rplogsumlem2  26063  dchrisumlem2  26068  dchrisum0lem1  26094  logdivbnd  26134  pntrsumbnd2  26145  pntrlog2bndlem1  26155  pntpbnd1  26164  pntpbnd2  26165  pntlemh  26177  pntlemj  26181  axlowdimlem17  26746  fzsplit3  30519  swrdrn2  30630  swrdrn3  30631  swrdf1  30632  swrdrndisj  30633  ballotlemfrci  31787  subfacp1lem3  32431  knoppcnlem11  33844  poimirlem1  34895  poimirlem2  34896  poimirlem31  34925  poimirlem32  34926  mblfinlem2  34932  mettrifi  35034  geomcau  35036  iunincfi  41367  elfzfzo  41549  fsumsermpt  41867  fmulcl  41869  fmuldfeqlem1  41870  iblspltprt  42265  itgspltprt  42271  stoweidlem11  42303  stoweidlem17  42309  stirlinglem7  42372  fourierdlem15  42414  fourierdlem25  42424  sge0isum  42716  sge0seq  42735  sge0reuz  42736  sge0reuzb  42737  iundjiun  42749  meaiuninclem  42769  carageniuncllem1  42810  carageniuncllem2  42811  caratheodorylem1  42815  ssfz12  43521  iccpartgt  43594