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

Theorem elfzuz 12376
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 12374 . 2 (𝐾 ∈ (𝑀...𝑁) ↔ (𝐾 ∈ (ℤ𝑀) ∧ 𝑁 ∈ (ℤ𝐾)))
21simplbi 475 1 (𝐾 ∈ (𝑀...𝑁) → 𝐾 ∈ (ℤ𝑀))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2030  cfv 5926  (class class class)co 6690  cuz 11725  ...cfz 12364
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-fv 5934  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-1st 7210  df-2nd 7211  df-neg 10307  df-z 11416  df-uz 11726  df-fz 12365
This theorem is referenced by:  elfzel1  12379  elfzelz  12380  elfzle1  12382  eluzfz2b  12388  fzsplit2  12404  fzsplit  12405  fzopth  12416  fzss1  12418  fzss2  12419  fzssuz  12420  fzp1elp1  12432  uzsplit  12450  elfzmlbm  12488  predfz  12503  fzosplit  12540  seqf2  12860  seqfeq2  12864  seqfeq  12866  sermono  12873  seqf1olem2  12881  seqz  12889  seqfeq3  12891  ser0  12893  seqcoll  13286  swrdval2  13465  swrd0val  13466  swrdswrd  13506  swrdccatin12  13537  splid  13550  spllen  13551  splfv1  13552  limsupgre  14256  clim2ser  14429  clim2ser2  14430  isermulc2  14432  iserle  14434  climub  14436  isercolllem1  14439  isercolllem3  14441  isercoll2  14443  iseraltlem1  14456  fsumcvg  14487  fsumser  14505  isumclim3  14534  isumadd  14542  fsump1i  14544  fsum0diaglem  14552  o1fsum  14589  iserabs  14591  cvgcmp  14592  cvgcmpub  14593  cvgcmpce  14594  isumsplit  14616  isum1p  14617  isumsup2  14622  climcndslem1  14625  climcndslem2  14626  climcnds  14627  geoserg  14642  mertenslem1  14660  clim2div  14665  prodf1  14667  prodfn0  14670  ntrivcvgmullem  14677  fprodcvg  14704  fprodntriv  14716  fprodabs  14748  fprodeq0  14749  iprodclim3  14775  iprodmul  14778  fprodefsum  14869  prmind2  15445  prmdvdsfz  15464  pcfac  15650  prmreclem4  15670  prmreclem5  15671  prmgaplem1  15800  prmgaplem2  15801  prmgaplcmlem2  15803  prmgapprmolem  15812  efgtlen  18185  efgredleme  18202  efgredlemc  18204  frgpuplem  18231  ovolunlem1a  23310  ovolicc1  23330  uniioombllem3  23399  dvfsumrlimf  23833  dvfsumlem1  23834  dvfsumlem2  23835  dvfsumlem3  23836  dvfsumlem4  23837  dvfsum2  23842  coeidlem  24038  coeid3  24041  vieta1lem2  24111  mtest  24203  mtestbdd  24204  birthdaylem2  24724  wilth  24842  ftalem4  24847  ftalem5  24848  chtub  24982  mersenne  24997  bposlem6  25059  lgsdilem2  25103  rplogsumlem1  25218  rplogsumlem2  25219  dchrisumlem2  25224  dchrisum0lem1  25250  logdivbnd  25290  pntrsumbnd2  25301  pntrlog2bndlem1  25311  pntpbnd1  25320  pntpbnd2  25321  pntlemh  25333  pntlemj  25337  axlowdimlem17  25883  fzsplit3  29681  ballotlemfrci  30717  wrdsplex  30746  subfacp1lem3  31290  knoppcnlem11  32618  poimirlem1  33540  poimirlem2  33541  poimirlem31  33570  poimirlem32  33571  mblfinlem2  33577  mettrifi  33683  geomcau  33685  iunincfi  39586  elfzfzo  39802  fsumsermpt  40129  fmulcl  40131  fmuldfeqlem1  40132  iblspltprt  40507  itgspltprt  40513  stoweidlem11  40546  stoweidlem17  40552  stirlinglem7  40615  fourierdlem15  40657  fourierdlem25  40667  sge0isum  40962  sge0seq  40981  sge0reuz  40982  sge0reuzb  40983  iundjiun  40995  meaiuninclem  41015  carageniuncllem1  41056  carageniuncllem2  41057  caratheodorylem1  41061  ssfz12  41649  iccpartgt  41688  pfxccatin12  41750  pfxccatpfx2  41753
  Copyright terms: Public domain W3C validator