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

Theorem elfzuz3 12889
Description: Membership in a finite set of sequential integers implies membership in an upper set of integers. (Contributed by NM, 28-Sep-2005.) (Revised by Mario Carneiro, 28-Apr-2015.)
Assertion
Ref Expression
elfzuz3 (𝐾 ∈ (𝑀...𝑁) → 𝑁 ∈ (ℤ𝐾))

Proof of Theorem elfzuz3
StepHypRef Expression
1 elfzuzb 12886 . 2 (𝐾 ∈ (𝑀...𝑁) ↔ (𝐾 ∈ (ℤ𝑀) ∧ 𝑁 ∈ (ℤ𝐾)))
21simprbi 499 1 (𝐾 ∈ (𝑀...𝑁) → 𝑁 ∈ (ℤ𝐾))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2114  cfv 6331  (class class class)co 7133  cuz 12222  ...cfz 12876
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792  ax-sep 5179  ax-nul 5186  ax-pow 5242  ax-pr 5306  ax-un 7439  ax-cnex 10571  ax-resscn 10572
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-ne 3007  df-ral 3130  df-rex 3131  df-rab 3134  df-v 3475  df-sbc 3753  df-csb 3861  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4270  df-if 4444  df-pw 4517  df-sn 4544  df-pr 4546  df-op 4550  df-uni 4815  df-iun 4897  df-br 5043  df-opab 5105  df-mpt 5123  df-id 5436  df-xp 5537  df-rel 5538  df-cnv 5539  df-co 5540  df-dm 5541  df-rn 5542  df-res 5543  df-ima 5544  df-iota 6290  df-fun 6333  df-fn 6334  df-f 6335  df-fv 6339  df-ov 7136  df-oprab 7137  df-mpo 7138  df-1st 7667  df-2nd 7668  df-neg 10851  df-z 11961  df-uz 12223  df-fz 12877
This theorem is referenced by:  elfzel2  12890  elfzle2  12895  peano2fzr  12904  fzsplit2  12916  fzsplit  12917  fznn0sub  12923  fzopth  12928  fzss1  12930  fzss2  12931  fzp1elp1  12944  predfz  13016  fzosplit  13054  fzoend  13112  fzofzp1b  13119  uzindi  13334  seqcl2  13373  seqfveq2  13377  monoord  13385  sermono  13387  seqsplit  13388  seqf1olem2  13395  seqid2  13401  seqhomo  13402  seqz  13403  bcval5  13663  seqcoll  13807  seqcoll2  13808  swrdval2  13988  pfxres  14021  pfxf  14022  spllen  14096  splfv2a  14098  repswpfx  14127  fsum0diag2  15118  climcndslem2  15185  prodfn0  15230  lcmflefac  15970  pcbc  16214  vdwlem2  16296  vdwlem5  16299  vdwlem6  16300  vdwlem8  16302  prmgaplem1  16363  psgnunilem5  18601  efgsres  18843  efgredleme  18848  efgcpbllemb  18860  imasdsf1olem  22959  volsup  24139  dvn2bss  24512  dvtaylp  24944  wilth  25635  ftalem1  25637  ppisval2  25669  dvdsppwf1o  25750  logfaclbnd  25785  bposlem6  25852  wlkres  27439  fzsplit3  30504  wrdres  30600  pfxf1  30605  swrdrn2  30615  swrdrn3  30616  swrdf1  30617  swrdrndisj  30618  splfv3  30619  cycpmco2f1  30774  cycpmco2rn  30775  cycpmco2lem7  30782  ballotlemsima  31781  ballotlemfrc  31792  ballotlemfrceq  31794  fzssfzo  31817  signstres  31853  fsum2dsub  31886  revpfxsfxrev  32370  swrdrevpfx  32371  pfxwlk  32378  erdszelem7  32452  erdszelem8  32453  poimirlem1  34934  poimirlem2  34935  poimirlem3  34936  poimirlem4  34937  poimirlem7  34940  poimirlem12  34945  poimirlem15  34948  poimirlem16  34949  poimirlem17  34950  poimirlem19  34952  poimirlem20  34953  poimirlem23  34956  poimirlem24  34957  poimirlem25  34958  poimirlem29  34962  poimirlem31  34964  mettrifi  35071  bcc0  40827  iunincfi  41515  monoordxrv  41912  fmulcl  42014  fmul01lt1lem2  42018  dvnprodlem2  42380  stoweidlem11  42444  stoweidlem17  42450  fourierdlem15  42555  ssfz12  43662  smonoord  43679
  Copyright terms: Public domain W3C validator