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

Theorem elfz5 12588
Description: Membership in a finite set of sequential integers. (Contributed by NM, 26-Dec-2005.)
Assertion
Ref Expression
elfz5 ((𝐾 ∈ (ℤ𝑀) ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (𝑀...𝑁) ↔ 𝐾𝑁))

Proof of Theorem elfz5
StepHypRef Expression
1 eluzelz 11940 . . . 4 (𝐾 ∈ (ℤ𝑀) → 𝐾 ∈ ℤ)
2 eluzel2 11935 . . . 4 (𝐾 ∈ (ℤ𝑀) → 𝑀 ∈ ℤ)
31, 2jca 508 . . 3 (𝐾 ∈ (ℤ𝑀) → (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ))
4 elfz 12586 . . . 4 ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (𝑀...𝑁) ↔ (𝑀𝐾𝐾𝑁)))
543expa 1148 . . 3 (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (𝑀...𝑁) ↔ (𝑀𝐾𝐾𝑁)))
63, 5sylan 576 . 2 ((𝐾 ∈ (ℤ𝑀) ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (𝑀...𝑁) ↔ (𝑀𝐾𝐾𝑁)))
7 eluzle 11943 . . . 4 (𝐾 ∈ (ℤ𝑀) → 𝑀𝐾)
87biantrurd 529 . . 3 (𝐾 ∈ (ℤ𝑀) → (𝐾𝑁 ↔ (𝑀𝐾𝐾𝑁)))
98adantr 473 . 2 ((𝐾 ∈ (ℤ𝑀) ∧ 𝑁 ∈ ℤ) → (𝐾𝑁 ↔ (𝑀𝐾𝐾𝑁)))
106, 9bitr4d 274 1 ((𝐾 ∈ (ℤ𝑀) ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (𝑀...𝑁) ↔ 𝐾𝑁))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 385  wcel 2157   class class class wbr 4843  cfv 6101  (class class class)co 6878  cle 10364  cz 11666  cuz 11930  ...cfz 12580
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-8 2159  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2377  ax-ext 2777  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5097  ax-cnex 10280  ax-resscn 10281
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3or 1109  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-mo 2591  df-eu 2609  df-clab 2786  df-cleq 2792  df-clel 2795  df-nfc 2930  df-ne 2972  df-ral 3094  df-rex 3095  df-rab 3098  df-v 3387  df-sbc 3634  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4116  df-if 4278  df-pw 4351  df-sn 4369  df-pr 4371  df-op 4375  df-uni 4629  df-br 4844  df-opab 4906  df-mpt 4923  df-id 5220  df-xp 5318  df-rel 5319  df-cnv 5320  df-co 5321  df-dm 5322  df-rn 5323  df-res 5324  df-ima 5325  df-iota 6064  df-fun 6103  df-fn 6104  df-f 6105  df-fv 6109  df-ov 6881  df-oprab 6882  df-mpt2 6883  df-neg 10559  df-z 11667  df-uz 11931  df-fz 12581
This theorem is referenced by:  fzsplit2  12620  fznn0sub2  12701  predfz  12719  bcval5  13358  hashf1  13490  seqcoll  13497  limsupgre  14553  isercolllem2  14737  isercoll  14739  fsumcvg3  14801  fsum0diaglem  14846  climcndslem2  14920  mertenslem1  14953  ncoprmlnprm  15769  pcfac  15936  prmreclem2  15954  prmreclem3  15955  prmreclem5  15957  1arith  15964  vdwlem1  16018  vdwlem3  16020  vdwlem10  16027  sylow1lem1  18326  psrbaglefi  19695  ovoliunlem1  23610  ovolicc2lem4  23628  uniioombllem3  23693  mbfi1fseqlem3  23825  iblcnlem1  23895  plyeq0lem  24307  coeeulem  24321  coeidlem  24334  coeid3  24337  coeeq2  24339  coemulhi  24351  vieta1lem2  24407  birthdaylem2  25031  birthdaylem3  25032  ftalem5  25155  basellem2  25160  basellem3  25161  basellem5  25163  musum  25269  fsumvma2  25291  chpchtsum  25296  lgsne0  25412  lgsquadlem2  25458  rplogsumlem2  25526  dchrisumlem1  25530  dchrisum0lem1  25557  ostth2lem3  25676  eupth2lems  27583  fzsplit3  30071  eulerpartlems  30938  eulerpartlemb  30946  erdszelem7  31696  cvmliftlem7  31790
  Copyright terms: Public domain W3C validator