MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elfz5 Unicode version

Theorem elfz5 10983
Description: Membership in a finite set of sequential integers. (Contributed by NM, 26-Dec-2005.)
Assertion
Ref Expression
elfz5  |-  ( ( K  e.  ( ZZ>= `  M )  /\  N  e.  ZZ )  ->  ( K  e.  ( M ... N )  <->  K  <_  N ) )

Proof of Theorem elfz5
StepHypRef Expression
1 eluzelz 10428 . . . 4  |-  ( K  e.  ( ZZ>= `  M
)  ->  K  e.  ZZ )
2 eluzel2 10425 . . . 4  |-  ( K  e.  ( ZZ>= `  M
)  ->  M  e.  ZZ )
31, 2jca 519 . . 3  |-  ( K  e.  ( ZZ>= `  M
)  ->  ( K  e.  ZZ  /\  M  e.  ZZ ) )
4 elfz 10981 . . . 4  |-  ( ( K  e.  ZZ  /\  M  e.  ZZ  /\  N  e.  ZZ )  ->  ( K  e.  ( M ... N )  <->  ( M  <_  K  /\  K  <_  N ) ) )
543expa 1153 . . 3  |-  ( ( ( K  e.  ZZ  /\  M  e.  ZZ )  /\  N  e.  ZZ )  ->  ( K  e.  ( M ... N
)  <->  ( M  <_  K  /\  K  <_  N
) ) )
63, 5sylan 458 . 2  |-  ( ( K  e.  ( ZZ>= `  M )  /\  N  e.  ZZ )  ->  ( K  e.  ( M ... N )  <->  ( M  <_  K  /\  K  <_  N ) ) )
7 eluzle 10430 . . . 4  |-  ( K  e.  ( ZZ>= `  M
)  ->  M  <_  K )
87biantrurd 495 . . 3  |-  ( K  e.  ( ZZ>= `  M
)  ->  ( K  <_  N  <->  ( M  <_  K  /\  K  <_  N
) ) )
98adantr 452 . 2  |-  ( ( K  e.  ( ZZ>= `  M )  /\  N  e.  ZZ )  ->  ( K  <_  N  <->  ( M  <_  K  /\  K  <_  N ) ) )
106, 9bitr4d 248 1  |-  ( ( K  e.  ( ZZ>= `  M )  /\  N  e.  ZZ )  ->  ( K  e.  ( M ... N )  <->  K  <_  N ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359    e. wcel 1717   class class class wbr 4153   ` cfv 5394  (class class class)co 6020    <_ cle 9054   ZZcz 10214   ZZ>=cuz 10420   ...cfz 10975
This theorem is referenced by:  fzsplit2  11008  fznn0sub2  11018  bcval5  11536  hashf1  11633  seqcoll  11639  limsupgre  12202  isercolllem2  12386  isercoll  12388  fsumcvg3  12450  fsum0diaglem  12487  climcndslem2  12557  mertenslem1  12588  pcfac  13195  prmreclem2  13212  prmreclem3  13213  prmreclem5  13215  1arith  13222  vdwlem1  13276  vdwlem3  13278  vdwlem10  13285  sylow1lem1  15159  psrbaglefi  16364  ovoliunlem1  19265  ovolicc2lem4  19283  uniioombllem3  19344  mbfi1fseqlem3  19476  iblcnlem1  19546  plyeq0lem  19996  coeeulem  20010  coeidlem  20023  coeid3  20026  coeeq2  20028  coemulhi  20039  vieta1lem2  20095  birthdaylem2  20658  birthdaylem3  20659  ftalem5  20726  basellem2  20731  basellem3  20732  basellem5  20734  musum  20843  fsumvma2  20865  chpchtsum  20870  lgsne0  20984  lgsquadlem2  21006  rplogsumlem2  21046  dchrisumlem1  21050  dchrisum0lem1  21077  ostth2lem3  21196  constr3pthlem3  21492  eupath2lem3  21549  eupath2  21550  konigsberg  21557  fzsplit3  23986  erdszelem7  24662  cvmliftlem7  24757  predfz  25227
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-13 1719  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368  ax-sep 4271  ax-nul 4279  ax-pow 4318  ax-pr 4344  ax-cnex 8979  ax-resscn 8980
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2242  df-mo 2243  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-ne 2552  df-ral 2654  df-rex 2655  df-rab 2658  df-v 2901  df-sbc 3105  df-dif 3266  df-un 3268  df-in 3270  df-ss 3277  df-nul 3572  df-if 3683  df-pw 3744  df-sn 3763  df-pr 3764  df-op 3766  df-uni 3958  df-br 4154  df-opab 4208  df-mpt 4209  df-id 4439  df-xp 4824  df-rel 4825  df-cnv 4826  df-co 4827  df-dm 4828  df-rn 4829  df-res 4830  df-ima 4831  df-iota 5358  df-fun 5396  df-fn 5397  df-f 5398  df-fv 5402  df-ov 6023  df-oprab 6024  df-mpt2 6025  df-neg 9226  df-z 10215  df-uz 10421  df-fz 10976
  Copyright terms: Public domain W3C validator