Theorem elfzuz 13652

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ‘cfv 6538  (class class class)co 7420  ℤ_≥cuz 12965  ...cfz 13639

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391  ax-un 7751  ax-cnex 11256  ax-resscn 11257

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-fv 6546  df-ov 7423  df-oprab 7424  df-mpo 7425  df-1st 8001  df-2nd 8002  df-neg 11544  df-z 12694  df-uz 12966  df-fz 13640

This theorem is used by:  elfzel1  13655  elfzelz  13656  elfzle1  13660  eluzfz2b  13666  fzsplit2  13683  fzsplit  13684  fzopth  13695  fzss1  13697  fzss2  13698  fzssuz  13699  fzp1elp1  13711  uzsplit  13730  elfzmlbm  13772  predfz  13787  fzosplit  13827  seqf2  14164  seqfeq2  14168  seqfeq  14170  sermono  14177  seqf1olem2  14185  seqz  14193  seqfeq3  14195  ser0  14197  seqcoll  14609  swrdval2  14794  swrdf1  14799  swrdrn3  14802  swrdswrd  14854  pfxccatin12  14882  pfxccatpfx2  14886  spllen  14903  swrds2m  15092  limsupgre  15648  clim2ser  15822  clim2ser2  15823  isermulc2  15825  iserle  15827  climub  15829  isercolllem1  15832  isercolllem3  15834  isercoll2  15836  iseraltlem1  15849  fsumcvg  15878  fsumser  15896  isumclim3  15925  isumadd  15933  fsump1i  15935  fsum0diaglem  15942  o1fsum  15980  iserabs  15982  cvgcmp  15983  cvgcmpub  15984  cvgcmpce  15985  isumsplit  16009  isum1p  16010  isumsup2  16015  climcndslem1  16018  climcndslem2  16019  climcnds  16020  geoserg  16035  mertenslem1  16053  clim2div  16058  prodf1  16060  prodfn0  16063  ntrivcvgmullem  16070  fprodcvg  16097  fprodntriv  16109  fprodabs  16141  fprodeq0  16142  iprodclim3  16167  iprodmul  16170  fprodefsum  16261  prmind2  16860  prmdvdsfz  16881  pcfac  17077  prmreclem4  17097  prmreclem5  17098  prmgaplem1  17227  prmgaplem2  17228  prmgaplcmlem2  17230  prmgapprmolem  17239  efgtlen  19940  efgredleme  19957  ovolunlem1a  25817  ovolicc1  25837  uniioombllem3  25906  dvfsumrlimf  26345  dvfsumlem1  26346  dvfsumlem2  26347  dvfsumlem3  26348  dvfsumlem4  26349  dvfsum2  26354  coeidlem  26556  coeid3  26559  vieta1lem2  26634  mtest  26731  mtestbdd  26732  birthdaylem2  27280  wilth  27398  ftalem4  27403  ftalem5  27404  chtub  27539  mersenne  27554  bposlem6  27616  lgsdilem2  27660  rplogsumlem1  27811  rplogsumlem2  27812  dchrisumlem2  27817  dchrisum0lem1  27843  logdivbnd  27883  pntrsumbnd2  27894  pntrlog2bndlem1  27904  pntpbnd1  27913  pntpbnd2  27914  pntlemh  27926  pntlemj  27930  axlowdimlem17  29536  fzsplit3  33385  swrdrn2  33517  swrdrndisj  33518  ballotlemfrci  35160  subfacp1lem3  35947  knoppcnlem11  37369  poimirlem1  38539  poimirlem2  38540  poimirlem31  38569  poimirlem32  38570  mblfinlem2  38576  mettrifi  38691  geomcau  38693  fzsplitnd  43032  aks4d1p3  43128  iunincfi  46108  elfzfzo  46292  fsumsermpt  46590  fmulcl  46592  fmuldfeqlem1  46593  iblspltprt  46982  itgspltprt  46988  stoweidlem11  47020  stoweidlem17  47026  stirlinglem7  47089  fourierdlem15  47131  fourierdlem25  47141  sge0isum  47436  sge0seq  47455  sge0reuz  47456  sge0reuzb  47457  iundjiun  47469  meaiuninclem  47489  carageniuncllem1  47530  carageniuncllem2  47531  caratheodorylem1  47535  ssfz12  48383  iccpartgt  48508  indprmfz  48714