Theorem elfzuz 13474

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

Syntax hints:   → wi 4   ∈ wcel 2114  ‘cfv 6498  (class class class)co 7367  ℤ_≥cuz 12788  ...cfz 13461

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 2708  ax-sep 5231  ax-nul 5241  ax-pr 5375  ax-un 7689  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 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-iun 4935  df-br 5086  df-opab 5148  df-mpt 5167  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-fv 6506  df-ov 7370  df-oprab 7371  df-mpo 7372  df-1st 7942  df-2nd 7943  df-neg 11380  df-z 12525  df-uz 12789  df-fz 13462

This theorem is referenced by:  elfzel1  13477  elfzelz  13478  elfzle1  13481  eluzfz2b  13487  fzsplit2  13503  fzsplit  13504  fzopth  13515  fzss1  13517  fzss2  13518  fzssuz  13519  fzp1elp1  13531  uzsplit  13550  elfzmlbm  13592  predfz  13607  fzosplit  13647  seqf2  13983  seqfeq2  13987  seqfeq  13989  sermono  13996  seqf1olem2  14004  seqz  14012  seqfeq3  14014  ser0  14016  seqcoll  14426  swrdval2  14609  swrdswrd  14667  pfxccatin12  14695  pfxccatpfx2  14699  spllen  14716  swrds2m  14903  limsupgre  15443  clim2ser  15617  clim2ser2  15618  isermulc2  15620  iserle  15622  climub  15624  isercolllem1  15627  isercolllem3  15629  isercoll2  15631  iseraltlem1  15644  fsumcvg  15674  fsumser  15692  isumclim3  15721  isumadd  15729  fsump1i  15731  fsum0diaglem  15738  o1fsum  15776  iserabs  15778  cvgcmp  15779  cvgcmpub  15780  cvgcmpce  15781  isumsplit  15805  isum1p  15806  isumsup2  15811  climcndslem1  15814  climcndslem2  15815  climcnds  15816  geoserg  15831  mertenslem1  15849  clim2div  15854  prodf1  15856  prodfn0  15859  ntrivcvgmullem  15866  fprodcvg  15895  fprodntriv  15907  fprodabs  15939  fprodeq0  15940  iprodclim3  15965  iprodmul  15968  fprodefsum  16060  prmind2  16654  prmdvdsfz  16675  pcfac  16870  prmreclem4  16890  prmreclem5  16891  prmgaplem1  17020  prmgaplem2  17021  prmgaplcmlem2  17023  prmgapprmolem  17032  efgtlen  19701  efgredleme  19718  ovolunlem1a  25463  ovolicc1  25483  uniioombllem3  25552  dvfsumrlimf  25992  dvfsumlem1  25993  dvfsumlem2  25994  dvfsumlem3  25995  dvfsumlem4  25996  dvfsum2  26001  coeidlem  26202  coeid3  26205  vieta1lem2  26277  mtest  26369  mtestbdd  26370  birthdaylem2  26916  wilth  27034  ftalem4  27039  ftalem5  27040  chtub  27175  mersenne  27190  bposlem6  27252  lgsdilem2  27296  rplogsumlem1  27447  rplogsumlem2  27448  dchrisumlem2  27453  dchrisum0lem1  27479  logdivbnd  27519  pntrsumbnd2  27530  pntrlog2bndlem1  27540  pntpbnd1  27549  pntpbnd2  27550  pntlemh  27562  pntlemj  27566  axlowdimlem17  29027  fzsplit3  32866  swrdrn2  33014  swrdrn3  33015  swrdf1  33016  swrdrndisj  33017  ballotlemfrci  34672  subfacp1lem3  35364  knoppcnlem11  36763  poimirlem1  37942  poimirlem2  37943  poimirlem31  37972  poimirlem32  37973  mblfinlem2  37979  mettrifi  38078  geomcau  38080  fzsplitnd  42421  aks4d1p3  42517  iunincfi  45524  elfzfzo  45710  fsumsermpt  46009  fmulcl  46011  fmuldfeqlem1  46012  iblspltprt  46401  itgspltprt  46407  stoweidlem11  46439  stoweidlem17  46445  stirlinglem7  46508  fourierdlem15  46550  fourierdlem25  46560  sge0isum  46855  sge0seq  46874  sge0reuz  46875  sge0reuzb  46876  iundjiun  46888  meaiuninclem  46908  carageniuncllem1  46949  carageniuncllem2  46950  caratheodorylem1  46954  ssfz12  47762  iccpartgt  47887  indprmfz  48093