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

Theorem elfz5 11089
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 10534 . . . 4  |-  ( K  e.  ( ZZ>= `  M
)  ->  K  e.  ZZ )
2 eluzel2 10531 . . . 4  |-  ( K  e.  ( ZZ>= `  M
)  ->  M  e.  ZZ )
31, 2jca 520 . . 3  |-  ( K  e.  ( ZZ>= `  M
)  ->  ( K  e.  ZZ  /\  M  e.  ZZ ) )
4 elfz 11087 . . . 4  |-  ( ( K  e.  ZZ  /\  M  e.  ZZ  /\  N  e.  ZZ )  ->  ( K  e.  ( M ... N )  <->  ( M  <_  K  /\  K  <_  N ) ) )
543expa 1154 . . 3  |-  ( ( ( K  e.  ZZ  /\  M  e.  ZZ )  /\  N  e.  ZZ )  ->  ( K  e.  ( M ... N
)  <->  ( M  <_  K  /\  K  <_  N
) ) )
63, 5sylan 459 . 2  |-  ( ( K  e.  ( ZZ>= `  M )  /\  N  e.  ZZ )  ->  ( K  e.  ( M ... N )  <->  ( M  <_  K  /\  K  <_  N ) ) )
7 eluzle 10536 . . . 4  |-  ( K  e.  ( ZZ>= `  M
)  ->  M  <_  K )
87biantrurd 496 . . 3  |-  ( K  e.  ( ZZ>= `  M
)  ->  ( K  <_  N  <->  ( M  <_  K  /\  K  <_  N
) ) )
98adantr 453 . 2  |-  ( ( K  e.  ( ZZ>= `  M )  /\  N  e.  ZZ )  ->  ( K  <_  N  <->  ( M  <_  K  /\  K  <_  N ) ) )
106, 9bitr4d 249 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 178    /\ wa 360    e. wcel 1728   class class class wbr 4243   ` cfv 5489  (class class class)co 6117    <_ cle 9159   ZZcz 10320   ZZ>=cuz 10526   ...cfz 11081
This theorem is referenced by:  fzsplit2  11114  fznn0sub2  11124  bcval5  11647  hashf1  11744  seqcoll  11750  limsupgre  12313  isercolllem2  12497  isercoll  12499  fsumcvg3  12561  fsum0diaglem  12598  climcndslem2  12668  mertenslem1  12699  pcfac  13306  prmreclem2  13323  prmreclem3  13324  prmreclem5  13326  1arith  13333  vdwlem1  13387  vdwlem3  13389  vdwlem10  13396  sylow1lem1  15270  psrbaglefi  16475  ovoliunlem1  19436  ovolicc2lem4  19454  uniioombllem3  19515  mbfi1fseqlem3  19645  iblcnlem1  19715  plyeq0lem  20167  coeeulem  20181  coeidlem  20194  coeid3  20197  coeeq2  20199  coemulhi  20210  vieta1lem2  20266  birthdaylem2  20829  birthdaylem3  20830  ftalem5  20897  basellem2  20902  basellem3  20903  basellem5  20905  musum  21014  fsumvma2  21036  chpchtsum  21041  lgsne0  21155  lgsquadlem2  21177  rplogsumlem2  21217  dchrisumlem1  21221  dchrisum0lem1  21248  ostth2lem3  21367  constr3pthlem3  21682  eupath2lem3  21739  eupath2  21740  konigsberg  21747  fzsplit3  24185  erdszelem7  24918  cvmliftlem7  25013  predfz  25513
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1628  ax-9 1669  ax-8 1690  ax-13 1730  ax-14 1732  ax-6 1747  ax-7 1752  ax-11 1764  ax-12 1954  ax-ext 2424  ax-sep 4361  ax-nul 4369  ax-pow 4412  ax-pr 4438  ax-cnex 9084  ax-resscn 9085
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1661  df-eu 2292  df-mo 2293  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-ral 2717  df-rex 2718  df-rab 2721  df-v 2967  df-sbc 3171  df-dif 3312  df-un 3314  df-in 3316  df-ss 3323  df-nul 3617  df-if 3768  df-pw 3830  df-sn 3849  df-pr 3850  df-op 3852  df-uni 4045  df-br 4244  df-opab 4298  df-mpt 4299  df-id 4533  df-xp 4919  df-rel 4920  df-cnv 4921  df-co 4922  df-dm 4923  df-rn 4924  df-res 4925  df-ima 4926  df-iota 5453  df-fun 5491  df-fn 5492  df-f 5493  df-fv 5497  df-ov 6120  df-oprab 6121  df-mpt2 6122  df-neg 9332  df-z 10321  df-uz 10527  df-fz 11082
  Copyright terms: Public domain W3C validator