Theorem elfzuz 13542

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

Syntax hints:   → wi 4   ∈ wcel 2107  ‘cfv 6541  (class class class)co 7413  ℤ_≥cuz 12860  ...cfz 13529

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-sep 5276  ax-nul 5286  ax-pr 5412  ax-un 7737  ax-cnex 11193  ax-resscn 11194

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ral 3051  df-rex 3060  df-rab 3420  df-v 3465  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4888  df-iun 4973  df-br 5124  df-opab 5186  df-mpt 5206  df-id 5558  df-xp 5671  df-rel 5672  df-cnv 5673  df-co 5674  df-dm 5675  df-rn 5676  df-res 5677  df-ima 5678  df-iota 6494  df-fun 6543  df-fn 6544  df-f 6545  df-fv 6549  df-ov 7416  df-oprab 7417  df-mpo 7418  df-1st 7996  df-2nd 7997  df-neg 11477  df-z 12597  df-uz 12861  df-fz 13530

This theorem is referenced by:  elfzel1  13545  elfzelz  13546  elfzle1  13549  eluzfz2b  13555  fzsplit2  13571  fzsplit  13572  fzopth  13583  fzss1  13585  fzss2  13586  fzssuz  13587  fzp1elp1  13599  uzsplit  13618  elfzmlbm  13660  predfz  13675  fzosplit  13714  seqf2  14044  seqfeq2  14048  seqfeq  14050  sermono  14057  seqf1olem2  14065  seqz  14073  seqfeq3  14075  ser0  14077  seqcoll  14486  swrdval2  14667  swrdswrd  14726  pfxccatin12  14754  pfxccatpfx2  14758  spllen  14775  swrds2m  14963  limsupgre  15500  clim2ser  15674  clim2ser2  15675  isermulc2  15677  iserle  15679  climub  15681  isercolllem1  15684  isercolllem3  15686  isercoll2  15688  iseraltlem1  15701  fsumcvg  15731  fsumser  15749  isumclim3  15778  isumadd  15786  fsump1i  15788  fsum0diaglem  15795  o1fsum  15832  iserabs  15834  cvgcmp  15835  cvgcmpub  15836  cvgcmpce  15837  isumsplit  15859  isum1p  15860  isumsup2  15865  climcndslem1  15868  climcndslem2  15869  climcnds  15870  geoserg  15885  mertenslem1  15903  clim2div  15908  prodf1  15910  prodfn0  15913  ntrivcvgmullem  15920  fprodcvg  15949  fprodntriv  15961  fprodabs  15993  fprodeq0  15994  iprodclim3  16019  iprodmul  16022  fprodefsum  16114  prmind2  16705  prmdvdsfz  16725  pcfac  16920  prmreclem4  16940  prmreclem5  16941  prmgaplem1  17070  prmgaplem2  17071  prmgaplcmlem2  17073  prmgapprmolem  17082  efgtlen  19713  efgredleme  19730  ovolunlem1a  25468  ovolicc1  25488  uniioombllem3  25557  dvfsumrlimf  26002  dvfsumlem1  26003  dvfsumlem2  26004  dvfsumlem2OLD  26005  dvfsumlem3  26006  dvfsumlem4  26007  dvfsum2  26012  coeidlem  26213  coeid3  26216  vieta1lem2  26290  mtest  26384  mtestbdd  26385  birthdaylem2  26932  wilth  27051  ftalem4  27056  ftalem5  27057  chtub  27193  mersenne  27208  bposlem6  27270  lgsdilem2  27314  rplogsumlem1  27465  rplogsumlem2  27466  dchrisumlem2  27471  dchrisum0lem1  27497  logdivbnd  27537  pntrsumbnd2  27548  pntrlog2bndlem1  27558  pntpbnd1  27567  pntpbnd2  27568  pntlemh  27580  pntlemj  27584  axlowdimlem17  28904  fzsplit3  32739  swrdrn2  32884  swrdrn3  32885  swrdf1  32886  swrdrndisj  32887  ballotlemfrci  34505  subfacp1lem3  35162  knoppcnlem11  36479  poimirlem1  37603  poimirlem2  37604  poimirlem31  37633  poimirlem32  37634  mblfinlem2  37640  mettrifi  37739  geomcau  37741  fzsplitnd  41958  aks4d1p3  42054  iunincfi  45071  elfzfzo  45260  fsumsermpt  45566  fmulcl  45568  fmuldfeqlem1  45569  iblspltprt  45960  itgspltprt  45966  stoweidlem11  45998  stoweidlem17  46004  stirlinglem7  46067  fourierdlem15  46109  fourierdlem25  46119  sge0isum  46414  sge0seq  46433  sge0reuz  46434  sge0reuzb  46435  iundjiun  46447  meaiuninclem  46467  carageniuncllem1  46508  carageniuncllem2  46509  caratheodorylem1  46513  ssfz12  47299  iccpartgt  47387