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

Theorem elfz5 12888
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 12241 . . . 4 (𝐾 ∈ (ℤ𝑀) → 𝐾 ∈ ℤ)
2 eluzel2 12236 . . . 4 (𝐾 ∈ (ℤ𝑀) → 𝑀 ∈ ℤ)
31, 2jca 512 . . 3 (𝐾 ∈ (ℤ𝑀) → (𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ))
4 elfz 12886 . . . 4 ((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (𝑀...𝑁) ↔ (𝑀𝐾𝐾𝑁)))
543expa 1110 . . 3 (((𝐾 ∈ ℤ ∧ 𝑀 ∈ ℤ) ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (𝑀...𝑁) ↔ (𝑀𝐾𝐾𝑁)))
63, 5sylan 580 . 2 ((𝐾 ∈ (ℤ𝑀) ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (𝑀...𝑁) ↔ (𝑀𝐾𝐾𝑁)))
7 eluzle 12244 . . . 4 (𝐾 ∈ (ℤ𝑀) → 𝑀𝐾)
87biantrurd 533 . . 3 (𝐾 ∈ (ℤ𝑀) → (𝐾𝑁 ↔ (𝑀𝐾𝐾𝑁)))
98adantr 481 . 2 ((𝐾 ∈ (ℤ𝑀) ∧ 𝑁 ∈ ℤ) → (𝐾𝑁 ↔ (𝑀𝐾𝐾𝑁)))
106, 9bitr4d 283 1 ((𝐾 ∈ (ℤ𝑀) ∧ 𝑁 ∈ ℤ) → (𝐾 ∈ (𝑀...𝑁) ↔ 𝐾𝑁))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  wcel 2105   class class class wbr 5057  cfv 6348  (class class class)co 7145  cle 10664  cz 11969  cuz 12231  ...cfz 12880
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-cnex 10581  ax-resscn 10582
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-ral 3140  df-rex 3141  df-rab 3144  df-v 3494  df-sbc 3770  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-br 5058  df-opab 5120  df-mpt 5138  df-id 5453  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-fv 6356  df-ov 7148  df-oprab 7149  df-mpo 7150  df-neg 10861  df-z 11970  df-uz 12232  df-fz 12881
This theorem is referenced by:  fzsplit2  12920  fznn0sub2  13002  predfz  13020  bcval5  13666  hashf1  13803  seqcoll  13810  limsupgre  14826  isercolllem2  15010  isercoll  15012  fsumcvg3  15074  fsum0diaglem  15119  climcndslem2  15193  mertenslem1  15228  ncoprmlnprm  16056  pcfac  16223  prmreclem2  16241  prmreclem3  16242  prmreclem5  16244  1arith  16251  vdwlem1  16305  vdwlem3  16307  vdwlem10  16314  sylow1lem1  18652  psrbaglefi  20080  ovoliunlem1  24030  ovolicc2lem4  24048  uniioombllem3  24113  mbfi1fseqlem3  24245  plyeq0lem  24727  coeeulem  24741  coeidlem  24754  coeid3  24757  coeeq2  24759  coemulhi  24771  vieta1lem2  24827  birthdaylem2  25457  birthdaylem3  25458  ftalem5  25581  basellem2  25586  basellem3  25587  basellem5  25589  musum  25695  fsumvma2  25717  chpchtsum  25722  lgsne0  25838  lgsquadlem2  25884  rplogsumlem2  25988  dchrisumlem1  25992  dchrisum0lem1  26019  ostth2lem3  26138  eupth2lems  27944  fzsplit3  30443  eulerpartlems  31517  eulerpartlemb  31525  erdszelem7  32341  cvmliftlem7  32435
  Copyright terms: Public domain W3C validator