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

Theorem elfz5 11555
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 10974 . . . 4  |-  ( K  e.  ( ZZ>= `  M
)  ->  K  e.  ZZ )
2 eluzel2 10970 . . . 4  |-  ( K  e.  ( ZZ>= `  M
)  ->  M  e.  ZZ )
31, 2jca 532 . . 3  |-  ( K  e.  ( ZZ>= `  M
)  ->  ( K  e.  ZZ  /\  M  e.  ZZ ) )
4 elfz 11553 . . . 4  |-  ( ( K  e.  ZZ  /\  M  e.  ZZ  /\  N  e.  ZZ )  ->  ( K  e.  ( M ... N )  <->  ( M  <_  K  /\  K  <_  N ) ) )
543expa 1188 . . 3  |-  ( ( ( K  e.  ZZ  /\  M  e.  ZZ )  /\  N  e.  ZZ )  ->  ( K  e.  ( M ... N
)  <->  ( M  <_  K  /\  K  <_  N
) ) )
63, 5sylan 471 . 2  |-  ( ( K  e.  ( ZZ>= `  M )  /\  N  e.  ZZ )  ->  ( K  e.  ( M ... N )  <->  ( M  <_  K  /\  K  <_  N ) ) )
7 eluzle 10977 . . . 4  |-  ( K  e.  ( ZZ>= `  M
)  ->  M  <_  K )
87biantrurd 508 . . 3  |-  ( K  e.  ( ZZ>= `  M
)  ->  ( K  <_  N  <->  ( M  <_  K  /\  K  <_  N
) ) )
98adantr 465 . 2  |-  ( ( K  e.  ( ZZ>= `  M )  /\  N  e.  ZZ )  ->  ( K  <_  N  <->  ( M  <_  K  /\  K  <_  N ) ) )
106, 9bitr4d 256 1  |-  ( ( K  e.  ( ZZ>= `  M )  /\  N  e.  ZZ )  ->  ( K  e.  ( M ... N )  <->  K  <_  N ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    e. wcel 1758   class class class wbr 4393   ` cfv 5519  (class class class)co 6193    <_ cle 9523   ZZcz 10750   ZZ>=cuz 10965   ...cfz 11547
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-sep 4514  ax-nul 4522  ax-pow 4571  ax-pr 4632  ax-cnex 9442  ax-resscn 9443
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-mo 2265  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-ral 2800  df-rex 2801  df-rab 2804  df-v 3073  df-sbc 3288  df-dif 3432  df-un 3434  df-in 3436  df-ss 3443  df-nul 3739  df-if 3893  df-pw 3963  df-sn 3979  df-pr 3981  df-op 3985  df-uni 4193  df-br 4394  df-opab 4452  df-mpt 4453  df-id 4737  df-xp 4947  df-rel 4948  df-cnv 4949  df-co 4950  df-dm 4951  df-rn 4952  df-res 4953  df-ima 4954  df-iota 5482  df-fun 5521  df-fn 5522  df-f 5523  df-fv 5527  df-ov 6196  df-oprab 6197  df-mpt2 6198  df-neg 9702  df-z 10751  df-uz 10966  df-fz 11548
This theorem is referenced by:  fzsplit2  11584  fznn0sub2  11598  bcval5  12204  hashf1  12321  seqcoll  12327  limsupgre  13070  isercolllem2  13254  isercoll  13256  fsumcvg3  13317  fsum0diaglem  13354  climcndslem2  13424  mertenslem1  13455  pcfac  14072  prmreclem2  14089  prmreclem3  14090  prmreclem5  14092  1arith  14099  vdwlem1  14153  vdwlem3  14155  vdwlem10  14162  sylow1lem1  16210  psrbaglefi  17556  psrbaglefiOLD  17557  ovoliunlem1  21110  ovolicc2lem4  21128  uniioombllem3  21191  mbfi1fseqlem3  21321  iblcnlem1  21391  plyeq0lem  21804  coeeulem  21818  coeidlem  21831  coeid3  21834  coeeq2  21836  coemulhi  21847  vieta1lem2  21903  birthdaylem2  22472  birthdaylem3  22473  ftalem5  22540  basellem2  22545  basellem3  22546  basellem5  22548  musum  22657  fsumvma2  22679  chpchtsum  22684  lgsne0  22798  lgsquadlem2  22820  rplogsumlem2  22860  dchrisumlem1  22864  dchrisum0lem1  22891  ostth2lem3  23010  constr3pthlem3  23688  eupath2lem3  23745  eupath2  23746  konigsberg  23753  fzsplit3  26216  eulerpartlems  26880  eulerpartlemb  26888  erdszelem7  27222  cvmliftlem7  27317  predfz  27801
  Copyright terms: Public domain W3C validator