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

Theorem elfz 11051
Description: Membership in a finite set of sequential integers. (Contributed by NM, 29-Sep-2005.)
Assertion
Ref Expression
elfz  |-  ( ( K  e.  ZZ  /\  M  e.  ZZ  /\  N  e.  ZZ )  ->  ( K  e.  ( M ... N )  <->  ( M  <_  K  /\  K  <_  N ) ) )

Proof of Theorem elfz
StepHypRef Expression
1 elfz1 11050 . . . 4  |-  ( ( M  e.  ZZ  /\  N  e.  ZZ )  ->  ( K  e.  ( M ... N )  <-> 
( K  e.  ZZ  /\  M  <_  K  /\  K  <_  N ) ) )
2 3anass 941 . . . . 5  |-  ( ( K  e.  ZZ  /\  M  <_  K  /\  K  <_  N )  <->  ( K  e.  ZZ  /\  ( M  <_  K  /\  K  <_  N ) ) )
32baib 873 . . . 4  |-  ( K  e.  ZZ  ->  (
( K  e.  ZZ  /\  M  <_  K  /\  K  <_  N )  <->  ( M  <_  K  /\  K  <_  N ) ) )
41, 3sylan9bb 682 . . 3  |-  ( ( ( M  e.  ZZ  /\  N  e.  ZZ )  /\  K  e.  ZZ )  ->  ( K  e.  ( M ... N
)  <->  ( M  <_  K  /\  K  <_  N
) ) )
543impa 1149 . 2  |-  ( ( M  e.  ZZ  /\  N  e.  ZZ  /\  K  e.  ZZ )  ->  ( K  e.  ( M ... N )  <->  ( M  <_  K  /\  K  <_  N ) ) )
653comr 1162 1  |-  ( ( K  e.  ZZ  /\  M  e.  ZZ  /\  N  e.  ZZ )  ->  ( K  e.  ( M ... N )  <->  ( M  <_  K  /\  K  <_  N ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    /\ wa 360    /\ w3a 937    e. wcel 1726   class class class wbr 4214  (class class class)co 6083    <_ cle 9123   ZZcz 10284   ...cfz 11045
This theorem is referenced by:  elfz5  11053  fzrev  11110  fzctr  11119  elfzo  11144  seqf1olem1  11364  bcval5  11611  isprm3  13090  hashdvds  13166  eulerthlem2  13173  prmreclem5  13290  aannenlem1  20247  basellem3  20867  chtub  20998  bcmono  21063  bposlem1  21070  lgseisenlem1  21135  lgsquadlem1  21140  constr3trllem3  21641  fznatpl1  25200  axlowdimlem3  25885  axlowdimlem7  25889  axlowdimlem16  25898  axlowdimlem17  25899  axlowdim  25902  mblfinlem2  26246  itg2addnclem2  26259  fzmul  26446  fzadd2  26447  cntotbnd  26507  fzsplit1nn0  26814  irrapxlem3  26889  pellexlem5  26898  acongrep  27047  fzneg  27049  jm2.23  27069  fmul01  27688  fmuldfeq  27691  stoweidlem26  27753
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-sep 4332  ax-nul 4340  ax-pr 4405  ax-cnex 9048  ax-resscn 9049
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 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2712  df-rex 2713  df-rab 2716  df-v 2960  df-sbc 3164  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-sn 3822  df-pr 3823  df-op 3825  df-uni 4018  df-br 4215  df-opab 4269  df-id 4500  df-xp 4886  df-rel 4887  df-cnv 4888  df-co 4889  df-dm 4890  df-iota 5420  df-fun 5458  df-fv 5464  df-ov 6086  df-oprab 6087  df-mpt2 6088  df-neg 9296  df-z 10285  df-fz 11046
  Copyright terms: Public domain W3C validator