Theorem elfzuz 13548

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

Syntax hints:   → wi 4   ∈ wcel 2149  ‘cfv 6537  (class class class)co 7411  ℤ_≥cuz 12862  ...cfz 13535

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-nul 5271  ax-pr 5405  ax-un 7733  ax-cnex 11156  ax-resscn 11157

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-iun 4962  df-br 5114  df-opab 5178  df-mpt 5197  df-id 5557  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-fv 6545  df-ov 7414  df-oprab 7415  df-mpo 7416  df-1st 7986  df-2nd 7987  df-neg 11444  df-z 12592  df-uz 12863  df-fz 13536

This theorem is referenced by:  elfzel1  13551  elfzelz  13552  elfzle1  13555  eluzfz2b  13561  fzsplit2  13577  fzsplit  13578  fzopth  13589  fzss1  13591  fzss2  13592  fzssuz  13593  fzp1elp1  13605  uzsplit  13624  elfzmlbm  13666  predfz  13681  fzosplit  13721  seqf2  14057  seqfeq2  14061  seqfeq  14063  sermono  14070  seqf1olem2  14078  seqz  14086  seqfeq3  14088  ser0  14090  seqcoll  14501  swrdval2  14684  swrdswrd  14742  pfxccatin12  14770  pfxccatpfx2  14774  spllen  14791  swrds2m  14978  limsupgre  15532  clim2ser  15706  clim2ser2  15707  isermulc2  15709  iserle  15711  climub  15713  isercolllem1  15716  isercolllem3  15718  isercoll2  15720  iseraltlem1  15733  fsumcvg  15763  fsumser  15781  isumclim3  15810  isumadd  15818  fsump1i  15820  fsum0diaglem  15827  o1fsum  15865  iserabs  15867  cvgcmp  15868  cvgcmpub  15869  cvgcmpce  15870  isumsplit  15894  isum1p  15895  isumsup2  15900  climcndslem1  15903  climcndslem2  15904  climcnds  15905  geoserg  15920  mertenslem1  15938  clim2div  15943  prodf1  15945  prodfn0  15948  ntrivcvgmullem  15955  fprodcvg  15984  fprodntriv  15996  fprodabs  16028  fprodeq0  16029  iprodclim3  16054  iprodmul  16057  fprodefsum  16149  prmind2  16743  prmdvdsfz  16764  pcfac  16959  prmreclem4  16979  prmreclem5  16980  prmgaplem1  17109  prmgaplem2  17110  prmgaplcmlem2  17112  prmgapprmolem  17121  efgtlen  19796  efgredleme  19813  ovolunlem1a  25624  ovolicc1  25644  uniioombllem3  25713  dvfsumrlimf  26153  dvfsumlem1  26154  dvfsumlem2  26155  dvfsumlem3  26156  dvfsumlem4  26157  dvfsum2  26162  coeidlem  26363  coeid3  26366  vieta1lem2  26441  mtest  26533  mtestbdd  26534  birthdaylem2  27083  wilth  27201  ftalem4  27206  ftalem5  27207  chtub  27342  mersenne  27357  bposlem6  27419  lgsdilem2  27463  rplogsumlem1  27614  rplogsumlem2  27615  dchrisumlem2  27620  dchrisum0lem1  27646  logdivbnd  27686  pntrsumbnd2  27697  pntrlog2bndlem1  27707  pntpbnd1  27716  pntpbnd2  27717  pntlemh  27729  pntlemj  27733  axlowdimlem17  29249  fzsplit3  33079  swrdrn2  33215  swrdrn3  33216  swrdf1  33217  swrdrndisj  33218  ballotlemfrci  34863  subfacp1lem3  35607  knoppcnlem11  37015  poimirlem1  38194  poimirlem2  38195  poimirlem31  38224  poimirlem32  38225  mblfinlem2  38231  mettrifi  38330  geomcau  38332  fzsplitnd  42673  aks4d1p3  42769  iunincfi  45738  elfzfzo  45922  fsumsermpt  46221  fmulcl  46223  fmuldfeqlem1  46224  iblspltprt  46613  itgspltprt  46619  stoweidlem11  46651  stoweidlem17  46657  stirlinglem7  46720  fourierdlem15  46762  fourierdlem25  46772  sge0isum  47067  sge0seq  47086  sge0reuz  47087  sge0reuzb  47088  iundjiun  47100  meaiuninclem  47120  carageniuncllem1  47161  carageniuncllem2  47162  caratheodorylem1  47166  ssfz12  47974  iccpartgt  48099  indprmfz  48305