Theorem elfzuz 13665

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  ‘cfv 6547  (class class class)co 7430  ℤ_≥cuz 12978  ...cfz 13652

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2196  ax-12 2215  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pr 5395  ax-un 7761  ax-cnex 11269  ax-resscn 11270

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2101  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-iun 4956  df-br 5107  df-opab 5171  df-mpt 5190  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 6501  df-fun 6549  df-fn 6550  df-f 6551  df-fv 6555  df-ov 7433  df-oprab 7434  df-mpo 7435  df-1st 8011  df-2nd 8012  df-neg 11557  df-z 12707  df-uz 12979  df-fz 13653

This theorem is used by:  elfzel1  13668  elfzelz  13669  elfzle1  13673  eluzfz2b  13679  fzsplit2  13696  fzsplit  13697  fzopth  13708  fzss1  13710  fzss2  13711  fzssuz  13712  fzp1elp1  13724  uzsplit  13743  elfzmlbm  13785  predfz  13800  fzosplit  13840  seqf2  14177  seqfeq2  14181  seqfeq  14183  sermono  14190  seqf1olem2  14198  seqz  14206  seqfeq3  14208  ser0  14210  seqcoll  14622  swrdval2  14808  swrdf1  14813  swrdrn3  14816  swrdswrd  14868  pfxccatin12  14896  pfxccatpfx2  14900  spllen  14917  swrds2m  15107  limsupgre  15663  clim2ser  15837  clim2ser2  15838  isermulc2  15840  iserle  15842  climub  15844  isercolllem1  15847  isercolllem3  15849  isercoll2  15851  iseraltlem1  15864  fsumcvg  15893  fsumser  15911  isumclim3  15940  isumadd  15948  fsump1i  15950  fsum0diaglem  15957  o1fsum  15995  iserabs  15997  cvgcmp  15998  cvgcmpub  15999  cvgcmpce  16000  isumsplit  16024  isum1p  16025  isumsup2  16030  climcndslem1  16033  climcndslem2  16034  climcnds  16035  geoserg  16050  mertenslem1  16068  clim2div  16073  prodf1  16075  prodfn0  16078  ntrivcvgmullem  16085  fprodcvg  16112  fprodntriv  16124  fprodabs  16156  fprodeq0  16157  iprodclim3  16182  iprodmul  16185  fprodefsum  16276  prmind2  16875  prmdvdsfz  16896  pcfac  17092  prmreclem4  17112  prmreclem5  17113  prmgaplem1  17242  prmgaplem2  17243  prmgaplcmlem2  17245  prmgapprmolem  17254  efgtlen  19955  efgredleme  19972  ovolunlem1a  25832  ovolicc1  25852  uniioombllem3  25921  dvfsumrlimf  26360  dvfsumlem1  26361  dvfsumlem2  26362  dvfsumlem3  26363  dvfsumlem4  26364  dvfsum2  26369  coeidlem  26571  coeid3  26574  vieta1lem2  26649  mtest  26746  mtestbdd  26747  birthdaylem2  27295  wilth  27413  ftalem4  27418  ftalem5  27419  chtub  27554  mersenne  27569  bposlem6  27631  lgsdilem2  27675  rplogsumlem1  27826  rplogsumlem2  27827  dchrisumlem2  27832  dchrisum0lem1  27858  logdivbnd  27898  pntrsumbnd2  27909  pntrlog2bndlem1  27919  pntpbnd1  27928  pntpbnd2  27929  pntlemh  27941  pntlemj  27945  axlowdimlem17  29551  fzsplit3  33441  swrdrn2  33573  swrdrndisj  33574  ballotlemfrci  35216  subfacp1lem3  36071  knoppcnlem11  37499  poimirlem1  38682  poimirlem2  38683  poimirlem31  38712  poimirlem32  38713  mblfinlem2  38719  mettrifi  38834  geomcau  38836  fzsplitnd  43175  aks4d1p3  43271  iunincfi  46251  elfzfzo  46435  fsumsermpt  46733  fmulcl  46735  fmuldfeqlem1  46736  iblspltprt  47125  itgspltprt  47131  stoweidlem11  47163  stoweidlem17  47169  stirlinglem7  47232  fourierdlem15  47274  fourierdlem25  47284  sge0isum  47579  sge0seq  47598  sge0reuz  47599  sge0reuzb  47600  iundjiun  47612  meaiuninclem  47632  carageniuncllem1  47673  carageniuncllem2  47674  caratheodorylem1  47678  ssfz12  48526  iccpartgt  48651  indprmfz  48857