MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elfzuz Structured version   Visualization version   GIF version

Theorem elfzuz 12277
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
StepHypRef Expression
1 elfzuzb 12275 . 2 (𝐾 ∈ (𝑀...𝑁) ↔ (𝐾 ∈ (ℤ𝑀) ∧ 𝑁 ∈ (ℤ𝐾)))
21simplbi 476 1 (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ (ℤ𝑀))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1992  cfv 5850  (class class class)co 6605  cuz 11631  ...cfz 12265
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-8 1994  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6903  ax-cnex 9937  ax-resscn 9938
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-eu 2478  df-mo 2479  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-ne 2797  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3193  df-sbc 3423  df-csb 3520  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-op 4160  df-uni 4408  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-id 4994  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-iota 5813  df-fun 5852  df-fn 5853  df-f 5854  df-fv 5858  df-ov 6608  df-oprab 6609  df-mpt2 6610  df-1st 7116  df-2nd 7117  df-neg 10214  df-z 11323  df-uz 11632  df-fz 12266
This theorem is referenced by:  elfzel1  12280  elfzelz  12281  elfzle1  12283  eluzfz2b  12289  fzsplit2  12305  fzsplit  12306  fzopth  12317  fzss1  12319  fzss2  12320  fzssuz  12321  fzp1elp1  12333  uzsplit  12350  elfzmlbm  12387  predfz  12402  fzosplit  12439  seqf2  12757  seqfeq2  12761  seqfeq  12763  sermono  12770  seqf1olem2  12778  seqz  12786  seqfeq3  12788  ser0  12790  seqcoll  13183  swrdval2  13353  swrd0val  13354  swrdswrd  13393  swrdccatin12  13423  splid  13436  spllen  13437  splfv1  13438  limsupgre  14141  clim2ser  14314  clim2ser2  14315  isermulc2  14317  iserle  14319  climub  14321  isercolllem1  14324  isercolllem3  14326  isercoll2  14328  iseraltlem1  14341  fsumcvg  14371  fsumser  14389  isumclim3  14413  isumadd  14421  fsump1i  14423  fsum0diaglem  14431  o1fsum  14467  iserabs  14469  cvgcmp  14470  cvgcmpub  14471  cvgcmpce  14472  isumsplit  14492  isum1p  14493  isumsup2  14498  climcndslem1  14501  climcndslem2  14502  climcnds  14503  geoserg  14518  mertenslem1  14536  clim2div  14541  prodf1  14543  prodfn0  14546  ntrivcvgmullem  14553  fprodcvg  14580  fprodntriv  14592  fprodabs  14624  fprodeq0  14625  iprodclim3  14651  iprodmul  14654  fprodefsum  14745  prmind2  15317  prmdvdsfz  15336  pcfac  15522  prmreclem4  15542  prmreclem5  15543  prmgaplem1  15672  prmgaplem2  15673  prmgaplcmlem2  15675  prmgapprmolem  15684  efgtlen  18055  efgredleme  18072  efgredlemc  18074  frgpuplem  18101  ovolunlem1a  23166  ovolicc1  23186  uniioombllem3  23254  dvfsumrlimf  23687  dvfsumlem1  23688  dvfsumlem2  23689  dvfsumlem3  23690  dvfsumlem4  23691  dvfsum2  23696  coeidlem  23892  coeid3  23895  vieta1lem2  23965  mtest  24057  mtestbdd  24058  birthdaylem2  24574  wilth  24692  ftalem4  24697  ftalem5  24698  chtub  24832  mersenne  24847  bposlem6  24909  lgsdilem2  24953  rplogsumlem1  25068  rplogsumlem2  25069  dchrisumlem2  25074  dchrisum0lem1  25100  logdivbnd  25140  pntrsumbnd2  25151  pntrlog2bndlem1  25161  pntpbnd1  25170  pntpbnd2  25171  pntlemh  25183  pntlemj  25187  axlowdimlem17  25733  fzsplit3  29386  ballotlemfrci  30362  wrdsplex  30390  subfacp1lem3  30864  knoppcnlem11  32127  poimirlem1  33028  poimirlem2  33029  poimirlem31  33058  poimirlem32  33059  mblfinlem2  33065  mettrifi  33171  geomcau  33173  iunincfi  38743  elfzfzo  38939  fsumsermpt  39202  fmulcl  39204  fmuldfeqlem1  39205  iblspltprt  39483  itgspltprt  39489  stoweidlem11  39522  stoweidlem17  39528  stirlinglem7  39591  fourierdlem15  39633  fourierdlem25  39643  sge0isum  39938  sge0seq  39957  sge0reuz  39958  sge0reuzb  39959  iundjiun  39971  meaiuninclem  39991  carageniuncllem1  40029  carageniuncllem2  40030  caratheodorylem1  40034  ssfz12  40609  iccpartgt  40649  pfxccatin12  40712  pfxccatpfx2  40715
  Copyright terms: Public domain W3C validator