Theorem elfzuz 12743

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

Syntax hints:   → wi 4   ∈ wcel 2079  ‘cfv 6217  (class class class)co 7007  ℤ_≥cuz 12082  ...cfz 12731

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886  ax-6 1945  ax-7 1990  ax-8 2081  ax-9 2089  ax-10 2110  ax-11 2124  ax-12 2139  ax-13 2342  ax-ext 2767  ax-sep 5088  ax-nul 5095  ax-pow 5150  ax-pr 5214  ax-un 7310  ax-cnex 10428  ax-resscn 10429

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1079  df-3an 1080  df-tru 1523  df-ex 1760  df-nf 1764  df-sb 2041  df-mo 2574  df-eu 2610  df-clab 2774  df-cleq 2786  df-clel 2861  df-nfc 2933  df-ne 2983  df-ral 3108  df-rex 3109  df-rab 3112  df-v 3434  df-sbc 3702  df-csb 3807  df-dif 3857  df-un 3859  df-in 3861  df-ss 3869  df-nul 4207  df-if 4376  df-pw 4449  df-sn 4467  df-pr 4469  df-op 4473  df-uni 4740  df-iun 4821  df-br 4957  df-opab 5019  df-mpt 5036  df-id 5340  df-xp 5441  df-rel 5442  df-cnv 5443  df-co 5444  df-dm 5445  df-rn 5446  df-res 5447  df-ima 5448  df-iota 6181  df-fun 6219  df-fn 6220  df-f 6221  df-fv 6225  df-ov 7010  df-oprab 7011  df-mpo 7012  df-1st 7536  df-2nd 7537  df-neg 10709  df-z 11819  df-uz 12083  df-fz 12732

This theorem is referenced by:  elfzel1  12746  elfzelz  12747  elfzle1  12749  eluzfz2b  12755  fzsplit2  12771  fzsplit  12772  fzopth  12783  fzss1  12785  fzss2  12786  fzssuz  12787  fzp1elp1  12799  uzsplit  12818  elfzmlbm  12856  predfz  12871  fzosplit  12908  seqf2  13227  seqfeq2  13231  seqfeq  13233  sermono  13240  seqf1olem2  13248  seqz  13256  seqfeq3  13258  ser0  13260  seqcoll  13658  swrdval2  13832  swrdswrd  13891  pfxccatin12  13919  pfxccatpfx2  13923  spllen  13940  swrds2m  14127  limsupgre  14660  clim2ser  14833  clim2ser2  14834  isermulc2  14836  iserle  14838  climub  14840  isercolllem1  14843  isercolllem3  14845  isercoll2  14847  iseraltlem1  14860  fsumcvg  14890  fsumser  14908  isumclim3  14935  isumadd  14943  fsump1i  14945  fsum0diaglem  14952  o1fsum  14989  iserabs  14991  cvgcmp  14992  cvgcmpub  14993  cvgcmpce  14994  isumsplit  15016  isum1p  15017  isumsup2  15022  climcndslem1  15025  climcndslem2  15026  climcnds  15027  geoserg  15042  mertenslem1  15061  clim2div  15066  prodf1  15068  prodfn0  15071  ntrivcvgmullem  15078  fprodcvg  15105  fprodntriv  15117  fprodabs  15149  fprodeq0  15150  iprodclim3  15175  iprodmul  15178  fprodefsum  15269  prmind2  15846  prmdvdsfz  15866  pcfac  16052  prmreclem4  16072  prmreclem5  16073  prmgaplem1  16202  prmgaplem2  16203  prmgaplcmlem2  16205  prmgapprmolem  16214  efgtlen  18567  efgredleme  18584  ovolunlem1a  23768  ovolicc1  23788  uniioombllem3  23857  dvfsumrlimf  24293  dvfsumlem1  24294  dvfsumlem2  24295  dvfsumlem3  24296  dvfsumlem4  24297  dvfsum2  24302  coeidlem  24498  coeid3  24501  vieta1lem2  24571  mtest  24663  mtestbdd  24664  birthdaylem2  25200  wilth  25318  ftalem4  25323  ftalem5  25324  chtub  25458  mersenne  25473  bposlem6  25535  lgsdilem2  25579  rplogsumlem1  25730  rplogsumlem2  25731  dchrisumlem2  25736  dchrisum0lem1  25762  logdivbnd  25802  pntrsumbnd2  25813  pntrlog2bndlem1  25823  pntpbnd1  25832  pntpbnd2  25833  pntlemh  25845  pntlemj  25849  axlowdimlem17  26415  fzsplit3  30175  ballotlemfrci  31358  subfacp1lem3  31993  knoppcnlem11  33395  poimirlem1  34370  poimirlem2  34371  poimirlem31  34400  poimirlem32  34401  mblfinlem2  34407  mettrifi  34510  geomcau  34512  iunincfi  40851  elfzfzo  41036  fsumsermpt  41356  fmulcl  41358  fmuldfeqlem1  41359  iblspltprt  41753  itgspltprt  41759  stoweidlem11  41792  stoweidlem17  41798  stirlinglem7  41861  fourierdlem15  41903  fourierdlem25  41913  sge0isum  42205  sge0seq  42224  sge0reuz  42225  sge0reuzb  42226  iundjiun  42238  meaiuninclem  42258  carageniuncllem1  42299  carageniuncllem2  42300  caratheodorylem1  42304  ssfz12  42984  iccpartgt  43023