Theorem elfzuz 13526

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

Syntax hints:   → wi 4   ∈ wcel 2143  ‘cfv 6522  (class class class)co 7397  ℤ_≥cuz 12840  ...cfz 13513

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5247  ax-nul 5257  ax-pr 5391  ax-un 7719  ax-cnex 11130  ax-resscn 11131

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1100  df-3an 1101  df-tru 1564  df-fal 1574  df-ex 1801  df-nf 1805  df-sb 2092  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3078  df-rex 3088  df-rab 3416  df-v 3457  df-sbc 3746  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-iun 4952  df-br 5102  df-opab 5164  df-mpt 5183  df-id 5543  df-xp 5654  df-rel 5655  df-cnv 5656  df-co 5657  df-dm 5658  df-rn 5659  df-res 5660  df-ima 5661  df-iota 6478  df-fun 6524  df-fn 6525  df-f 6526  df-fv 6530  df-ov 7400  df-oprab 7401  df-mpo 7402  df-1st 7971  df-2nd 7972  df-neg 11418  df-z 12570  df-uz 12841  df-fz 13514

This theorem is referenced by:  elfzel1  13529  elfzelz  13530  elfzle1  13533  eluzfz2b  13539  fzsplit2  13555  fzsplit  13556  fzopth  13567  fzss1  13569  fzss2  13570  fzssuz  13571  fzp1elp1  13583  uzsplit  13602  elfzmlbm  13644  predfz  13659  fzosplit  13699  seqf2  14035  seqfeq2  14039  seqfeq  14041  sermono  14048  seqf1olem2  14056  seqz  14064  seqfeq3  14066  ser0  14068  seqcoll  14478  swrdval2  14661  swrdswrd  14719  pfxccatin12  14747  pfxccatpfx2  14751  spllen  14768  swrds2m  14955  limsupgre  15509  clim2ser  15683  clim2ser2  15684  isermulc2  15686  iserle  15688  climub  15690  isercolllem1  15693  isercolllem3  15695  isercoll2  15697  iseraltlem1  15710  fsumcvg  15740  fsumser  15758  isumclim3  15787  isumadd  15795  fsump1i  15797  fsum0diaglem  15804  o1fsum  15842  iserabs  15844  cvgcmp  15845  cvgcmpub  15846  cvgcmpce  15847  isumsplit  15871  isum1p  15872  isumsup2  15877  climcndslem1  15880  climcndslem2  15881  climcnds  15882  geoserg  15897  mertenslem1  15915  clim2div  15920  prodf1  15922  prodfn0  15925  ntrivcvgmullem  15932  fprodcvg  15961  fprodntriv  15973  fprodabs  16005  fprodeq0  16006  iprodclim3  16031  iprodmul  16034  fprodefsum  16126  prmind2  16720  prmdvdsfz  16741  pcfac  16936  prmreclem4  16956  prmreclem5  16957  prmgaplem1  17086  prmgaplem2  17087  prmgaplcmlem2  17089  prmgapprmolem  17098  efgtlen  19767  efgredleme  19784  ovolunlem1a  25559  ovolicc1  25579  uniioombllem3  25648  dvfsumrlimf  26088  dvfsumlem1  26089  dvfsumlem2  26090  dvfsumlem3  26091  dvfsumlem4  26092  dvfsum2  26097  coeidlem  26298  coeid3  26301  vieta1lem2  26376  mtest  26468  mtestbdd  26469  birthdaylem2  27018  wilth  27136  ftalem4  27141  ftalem5  27142  chtub  27277  mersenne  27292  bposlem6  27354  lgsdilem2  27398  rplogsumlem1  27549  rplogsumlem2  27550  dchrisumlem2  27555  dchrisum0lem1  27581  logdivbnd  27621  pntrsumbnd2  27632  pntrlog2bndlem1  27642  pntpbnd1  27651  pntpbnd2  27652  pntlemh  27664  pntlemj  27668  axlowdimlem17  29160  fzsplit3  32996  swrdrn2  33133  swrdrn3  33134  swrdf1  33135  swrdrndisj  33136  ballotlemfrci  34826  subfacp1lem3  35533  knoppcnlem11  36942  poimirlem1  38121  poimirlem2  38122  poimirlem31  38151  poimirlem32  38152  mblfinlem2  38158  mettrifi  38257  geomcau  38259  fzsplitnd  42600  aks4d1p3  42696  iunincfi  45673  elfzfzo  45857  fsumsermpt  46156  fmulcl  46158  fmuldfeqlem1  46159  iblspltprt  46548  itgspltprt  46554  stoweidlem11  46586  stoweidlem17  46592  stirlinglem7  46655  fourierdlem15  46697  fourierdlem25  46707  sge0isum  47002  sge0seq  47021  sge0reuz  47022  sge0reuzb  47023  iundjiun  47035  meaiuninclem  47055  carageniuncllem1  47096  carageniuncllem2  47097  caratheodorylem1  47101  ssfz12  47909  iccpartgt  48034  indprmfz  48240