Theorem elfzuz 13434

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

Syntax hints:   → wi 4   ∈ wcel 2113  ‘cfv 6490  (class class class)co 7356  ℤ_≥cuz 12749  ...cfz 13421

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375  ax-un 7678  ax-cnex 11080  ax-resscn 11081

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ne 2931  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-sbc 3739  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-iun 4946  df-br 5097  df-opab 5159  df-mpt 5178  df-id 5517  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-fv 6498  df-ov 7359  df-oprab 7360  df-mpo 7361  df-1st 7931  df-2nd 7932  df-neg 11365  df-z 12487  df-uz 12750  df-fz 13422

This theorem is referenced by:  elfzel1  13437  elfzelz  13438  elfzle1  13441  eluzfz2b  13447  fzsplit2  13463  fzsplit  13464  fzopth  13475  fzss1  13477  fzss2  13478  fzssuz  13479  fzp1elp1  13491  uzsplit  13510  elfzmlbm  13552  predfz  13567  fzosplit  13606  seqf2  13942  seqfeq2  13946  seqfeq  13948  sermono  13955  seqf1olem2  13963  seqz  13971  seqfeq3  13973  ser0  13975  seqcoll  14385  swrdval2  14568  swrdswrd  14626  pfxccatin12  14654  pfxccatpfx2  14658  spllen  14675  swrds2m  14862  limsupgre  15402  clim2ser  15576  clim2ser2  15577  isermulc2  15579  iserle  15581  climub  15583  isercolllem1  15586  isercolllem3  15588  isercoll2  15590  iseraltlem1  15603  fsumcvg  15633  fsumser  15651  isumclim3  15680  isumadd  15688  fsump1i  15690  fsum0diaglem  15697  o1fsum  15734  iserabs  15736  cvgcmp  15737  cvgcmpub  15738  cvgcmpce  15739  isumsplit  15761  isum1p  15762  isumsup2  15767  climcndslem1  15770  climcndslem2  15771  climcnds  15772  geoserg  15787  mertenslem1  15805  clim2div  15810  prodf1  15812  prodfn0  15815  ntrivcvgmullem  15822  fprodcvg  15851  fprodntriv  15863  fprodabs  15895  fprodeq0  15896  iprodclim3  15921  iprodmul  15924  fprodefsum  16016  prmind2  16610  prmdvdsfz  16630  pcfac  16825  prmreclem4  16845  prmreclem5  16846  prmgaplem1  16975  prmgaplem2  16976  prmgaplcmlem2  16978  prmgapprmolem  16987  efgtlen  19653  efgredleme  19670  ovolunlem1a  25451  ovolicc1  25471  uniioombllem3  25540  dvfsumrlimf  25985  dvfsumlem1  25986  dvfsumlem2  25987  dvfsumlem2OLD  25988  dvfsumlem3  25989  dvfsumlem4  25990  dvfsum2  25995  coeidlem  26196  coeid3  26199  vieta1lem2  26273  mtest  26367  mtestbdd  26368  birthdaylem2  26916  wilth  27035  ftalem4  27040  ftalem5  27041  chtub  27177  mersenne  27192  bposlem6  27254  lgsdilem2  27298  rplogsumlem1  27449  rplogsumlem2  27450  dchrisumlem2  27455  dchrisum0lem1  27481  logdivbnd  27521  pntrsumbnd2  27532  pntrlog2bndlem1  27542  pntpbnd1  27551  pntpbnd2  27552  pntlemh  27564  pntlemj  27568  axlowdimlem17  28980  fzsplit3  32822  swrdrn2  32985  swrdrn3  32986  swrdf1  32987  swrdrndisj  32988  ballotlemfrci  34634  subfacp1lem3  35325  knoppcnlem11  36646  poimirlem1  37761  poimirlem2  37762  poimirlem31  37791  poimirlem32  37792  mblfinlem2  37798  mettrifi  37897  geomcau  37899  fzsplitnd  42175  aks4d1p3  42271  iunincfi  45280  elfzfzo  45467  fsumsermpt  45767  fmulcl  45769  fmuldfeqlem1  45770  iblspltprt  46159  itgspltprt  46165  stoweidlem11  46197  stoweidlem17  46203  stirlinglem7  46266  fourierdlem15  46308  fourierdlem25  46318  sge0isum  46613  sge0seq  46632  sge0reuz  46633  sge0reuzb  46634  iundjiun  46646  meaiuninclem  46666  carageniuncllem1  46707  carageniuncllem2  46708  caratheodorylem1  46712  ssfz12  47502  iccpartgt  47615