---

Step * of Lemma bag-summation-partitions-primes

∀[h:ℕ+ ⟶ ℕ+ ⟶ ℤ]. ∀[b:bag(Prime)].
  (Σ(p∈bag-partitions(IntDeq;b)). h[Π(fst(p));Π(snd(p))] = Σ i|Π(b). h[i;Π(b) ÷ i]  ∈ ℤ)
BY
{ xxx(Auto
      THEN (InstLemma `bag-summation-partitions-primes-general`  [⌜ℤ-rng⌝;⌜h⌝;⌜b⌝]⋅ THENA Auto)
      THEN Reduce (-1)
      THEN HypSubst' (-1) 0
      THEN RepUR ``let`` 0
      THEN Auto)xxx }

---

Latex:

---

Latex:
\mforall{}[h:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}].  \mforall{}[b:bag(Prime)].
    (\mSigma{}(p\mmember{}bag-partitions(IntDeq;b)).  h[\mPi{}(fst(p));\mPi{}(snd(p))]  =  \mSigma{}  i|\mPi{}(b).  h[i;\mPi{}(b)  \mdiv{}  i]  )


By

---

Latex:
xxx(Auto
        THEN  (InstLemma  `bag-summation-partitions-primes-general`    [\mkleeneopen{}\mBbbZ{}-rng\mkleeneclose{};\mkleeneopen{}h\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THENA  Auto)
        THEN  Reduce  (-1)
        THEN  HypSubst'  (-1)  0
        THEN  RepUR  ``let``  0
        THEN  Auto)xxx

---

Home Index