Theorem elfzuz 13577

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ‘cfv 6533  (class class class)co 7414  ℤ_≥cuz 12890  ...cfz 13564

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 2732  ax-sep 5251  ax-nul 5263  ax-pr 5398  ax-un 7737  ax-cnex 11183  ax-resscn 11184

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 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  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 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-fv 6541  df-ov 7417  df-oprab 7418  df-mpo 7419  df-1st 7987  df-2nd 7988  df-neg 11471  df-z 12619  df-uz 12891  df-fz 13565

This theorem is used by:  elfzel1  13580  elfzelz  13581  elfzle1  13584  eluzfz2b  13590  fzsplit2  13607  fzsplit  13608  fzopth  13619  fzss1  13621  fzss2  13622  fzssuz  13623  fzp1elp1  13635  uzsplit  13654  elfzmlbm  13696  predfz  13711  fzosplit  13751  seqf2  14088  seqfeq2  14092  seqfeq  14094  sermono  14101  seqf1olem2  14109  seqz  14117  seqfeq3  14119  ser0  14121  seqcoll  14532  swrdval2  14717  swrdf1  14722  swrdrn3  14725  swrdswrd  14777  pfxccatin12  14805  pfxccatpfx2  14809  spllen  14826  swrds2m  15015  limsupgre  15571  clim2ser  15745  clim2ser2  15746  isermulc2  15748  iserle  15750  climub  15752  isercolllem1  15755  isercolllem3  15757  isercoll2  15759  iseraltlem1  15772  fsumcvg  15801  fsumser  15819  isumclim3  15848  isumadd  15856  fsump1i  15858  fsum0diaglem  15865  o1fsum  15903  iserabs  15905  cvgcmp  15906  cvgcmpub  15907  cvgcmpce  15908  isumsplit  15932  isum1p  15933  isumsup2  15938  climcndslem1  15941  climcndslem2  15942  climcnds  15943  geoserg  15958  mertenslem1  15976  clim2div  15981  prodf1  15983  prodfn0  15986  ntrivcvgmullem  15993  fprodcvg  16020  fprodntriv  16032  fprodabs  16064  fprodeq0  16065  iprodclim3  16090  iprodmul  16093  fprodefsum  16184  prmind2  16778  prmdvdsfz  16799  pcfac  16994  prmreclem4  17014  prmreclem5  17015  prmgaplem1  17144  prmgaplem2  17145  prmgaplcmlem2  17147  prmgapprmolem  17156  efgtlen  19856  efgredleme  19873  ovolunlem1a  25727  ovolicc1  25747  uniioombllem3  25816  dvfsumrlimf  26255  dvfsumlem1  26256  dvfsumlem2  26257  dvfsumlem3  26258  dvfsumlem4  26259  dvfsum2  26264  coeidlem  26466  coeid3  26469  vieta1lem2  26546  mtest  26643  mtestbdd  26644  birthdaylem2  27192  wilth  27310  ftalem4  27315  ftalem5  27316  chtub  27451  mersenne  27466  bposlem6  27528  lgsdilem2  27572  rplogsumlem1  27723  rplogsumlem2  27724  dchrisumlem2  27729  dchrisum0lem1  27755  logdivbnd  27795  pntrsumbnd2  27806  pntrlog2bndlem1  27816  pntpbnd1  27825  pntpbnd2  27826  pntlemh  27838  pntlemj  27842  axlowdimlem17  29418  fzsplit3  33267  swrdrn2  33399  swrdrndisj  33400  ballotlemfrci  35042  subfacp1lem3  35764  knoppcnlem11  37203  poimirlem1  38373  poimirlem2  38374  poimirlem31  38403  poimirlem32  38404  mblfinlem2  38410  mettrifi  38510  geomcau  38512  fzsplitnd  42851  aks4d1p3  42947  iunincfi  45929  elfzfzo  46113  fsumsermpt  46412  fmulcl  46414  fmuldfeqlem1  46415  iblspltprt  46804  itgspltprt  46810  stoweidlem11  46842  stoweidlem17  46848  stirlinglem7  46911  fourierdlem15  46953  fourierdlem25  46963  sge0isum  47258  sge0seq  47277  sge0reuz  47278  sge0reuzb  47279  iundjiun  47291  meaiuninclem  47311  carageniuncllem1  47352  carageniuncllem2  47353  caratheodorylem1  47357  ssfz12  48205  iccpartgt  48330  indprmfz  48536