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

Theorem elfzuz3 12895
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 12892 . 2 (𝐾 ∈ (𝑀...𝑁) ↔ (𝐾 ∈ (ℤ𝑀) ∧ 𝑁 ∈ (ℤ𝐾)))
21simprbi 497 1 (𝐾 ∈ (𝑀...𝑁) → 𝑁 ∈ (ℤ𝐾))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2105  cfv 6349  (class class class)co 7145  cuz 12232  ...cfz 12882
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7450  ax-cnex 10582  ax-resscn 10583
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3497  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4833  df-iun 4914  df-br 5059  df-opab 5121  df-mpt 5139  df-id 5454  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-fv 6357  df-ov 7148  df-oprab 7149  df-mpo 7150  df-1st 7680  df-2nd 7681  df-neg 10862  df-z 11971  df-uz 12233  df-fz 12883
This theorem is referenced by:  elfzel2  12896  elfzle2  12901  peano2fzr  12910  fzsplit2  12922  fzsplit  12923  fznn0sub  12929  fzopth  12934  fzss1  12936  fzss2  12937  fzp1elp1  12950  predfz  13022  fzosplit  13060  fzoend  13118  fzofzp1b  13125  uzindi  13340  seqcl2  13378  seqfveq2  13382  monoord  13390  sermono  13392  seqsplit  13393  seqf1olem2  13400  seqid2  13406  seqhomo  13407  seqz  13408  bcval5  13668  seqcoll  13812  seqcoll2  13813  swrdval2  13998  pfxres  14031  pfxf  14032  spllen  14106  splfv2a  14108  repswpfx  14137  fsum0diag2  15128  climcndslem2  15195  prodfn0  15240  lcmflefac  15982  pcbc  16226  vdwlem2  16308  vdwlem5  16311  vdwlem6  16312  vdwlem8  16314  prmgaplem1  16375  psgnunilem5  18553  efgsres  18795  efgredleme  18800  efgcpbllemb  18812  imasdsf1olem  22912  volsup  24086  dvn2bss  24456  dvtaylp  24887  wilth  25576  ftalem1  25578  ppisval2  25610  dvdsppwf1o  25691  logfaclbnd  25726  bposlem6  25793  wlkres  27380  fzsplit3  30444  wrdres  30541  pfxf1  30546  swrdrn2  30556  swrdrn3  30557  swrdf1  30558  swrdrndisj  30559  splfv3  30560  cycpmco2f1  30694  cycpmco2rn  30695  cycpmco2lem7  30702  ballotlemsima  31673  ballotlemfrc  31684  ballotlemfrceq  31686  fzssfzo  31709  signstres  31745  fsum2dsub  31778  revpfxsfxrev  32260  swrdrevpfx  32261  pfxwlk  32268  erdszelem7  32342  erdszelem8  32343  poimirlem1  34775  poimirlem2  34776  poimirlem3  34777  poimirlem4  34778  poimirlem7  34781  poimirlem12  34786  poimirlem15  34789  poimirlem16  34790  poimirlem17  34791  poimirlem19  34793  poimirlem20  34794  poimirlem23  34797  poimirlem24  34798  poimirlem25  34799  poimirlem29  34803  poimirlem31  34805  mettrifi  34915  bcc0  40552  iunincfi  41240  monoordxrv  41638  fmulcl  41742  fmul01lt1lem2  41746  dvnprodlem2  42112  stoweidlem11  42177  stoweidlem17  42183  fourierdlem15  42288  ssfz12  43395  smonoord  43412
  Copyright terms: Public domain W3C validator