Theorem elfzuz 13448

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

Syntax hints:   → wi 4   ∈ wcel 2114  ‘cfv 6500  (class class class)co 7368  ℤ_≥cuz 12763  ...cfz 13435

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pr 5379  ax-un 7690  ax-cnex 11094  ax-resscn 11095

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-fv 6508  df-ov 7371  df-oprab 7372  df-mpo 7373  df-1st 7943  df-2nd 7944  df-neg 11379  df-z 12501  df-uz 12764  df-fz 13436

This theorem is referenced by:  elfzel1  13451  elfzelz  13452  elfzle1  13455  eluzfz2b  13461  fzsplit2  13477  fzsplit  13478  fzopth  13489  fzss1  13491  fzss2  13492  fzssuz  13493  fzp1elp1  13505  uzsplit  13524  elfzmlbm  13566  predfz  13581  fzosplit  13620  seqf2  13956  seqfeq2  13960  seqfeq  13962  sermono  13969  seqf1olem2  13977  seqz  13985  seqfeq3  13987  ser0  13989  seqcoll  14399  swrdval2  14582  swrdswrd  14640  pfxccatin12  14668  pfxccatpfx2  14672  spllen  14689  swrds2m  14876  limsupgre  15416  clim2ser  15590  clim2ser2  15591  isermulc2  15593  iserle  15595  climub  15597  isercolllem1  15600  isercolllem3  15602  isercoll2  15604  iseraltlem1  15617  fsumcvg  15647  fsumser  15665  isumclim3  15694  isumadd  15702  fsump1i  15704  fsum0diaglem  15711  o1fsum  15748  iserabs  15750  cvgcmp  15751  cvgcmpub  15752  cvgcmpce  15753  isumsplit  15775  isum1p  15776  isumsup2  15781  climcndslem1  15784  climcndslem2  15785  climcnds  15786  geoserg  15801  mertenslem1  15819  clim2div  15824  prodf1  15826  prodfn0  15829  ntrivcvgmullem  15836  fprodcvg  15865  fprodntriv  15877  fprodabs  15909  fprodeq0  15910  iprodclim3  15935  iprodmul  15938  fprodefsum  16030  prmind2  16624  prmdvdsfz  16644  pcfac  16839  prmreclem4  16859  prmreclem5  16860  prmgaplem1  16989  prmgaplem2  16990  prmgaplcmlem2  16992  prmgapprmolem  17001  efgtlen  19670  efgredleme  19687  ovolunlem1a  25468  ovolicc1  25488  uniioombllem3  25557  dvfsumrlimf  26002  dvfsumlem1  26003  dvfsumlem2  26004  dvfsumlem2OLD  26005  dvfsumlem3  26006  dvfsumlem4  26007  dvfsum2  26012  coeidlem  26213  coeid3  26216  vieta1lem2  26290  mtest  26384  mtestbdd  26385  birthdaylem2  26933  wilth  27052  ftalem4  27057  ftalem5  27058  chtub  27194  mersenne  27209  bposlem6  27271  lgsdilem2  27315  rplogsumlem1  27466  rplogsumlem2  27467  dchrisumlem2  27472  dchrisum0lem1  27498  logdivbnd  27538  pntrsumbnd2  27549  pntrlog2bndlem1  27559  pntpbnd1  27568  pntpbnd2  27569  pntlemh  27581  pntlemj  27585  axlowdimlem17  29047  fzsplit3  32888  swrdrn2  33051  swrdrn3  33052  swrdf1  33053  swrdrndisj  33054  ballotlemfrci  34710  subfacp1lem3  35402  knoppcnlem11  36729  poimirlem1  37876  poimirlem2  37877  poimirlem31  37906  poimirlem32  37907  mblfinlem2  37913  mettrifi  38012  geomcau  38014  fzsplitnd  42356  aks4d1p3  42452  iunincfi  45457  elfzfzo  45643  fsumsermpt  45943  fmulcl  45945  fmuldfeqlem1  45946  iblspltprt  46335  itgspltprt  46341  stoweidlem11  46373  stoweidlem17  46379  stirlinglem7  46442  fourierdlem15  46484  fourierdlem25  46494  sge0isum  46789  sge0seq  46808  sge0reuz  46809  sge0reuzb  46810  iundjiun  46822  meaiuninclem  46842  carageniuncllem1  46883  carageniuncllem2  46884  caratheodorylem1  46888  ssfz12  47678  iccpartgt  47791