---

Step * of Lemma bag-summation-partitions-primes-general

∀[r:CRng]. ∀[h:ℕ+ ⟶ ℕ+ ⟶ |r|]. ∀[b:bag(Prime)].
  (Σ(p∈bag-partitions(IntDeq;b)). h[Π(fst(p));Π(snd(p))] = let n = Π(b) in Σ i|n. h[i;n ÷ i] ∈ |r|)
BY
{ xxx(Unfold `gen-divisors-sum` 0
      THEN xxx(Auto
               THEN (Assert IntDeq ∈ EqDecider(Prime) BY
                           ((DoSubsume THEN Auto) THEN BLemma `strong-subtype-deq-subtype` THEN Auto))
               THEN RepUR ``let`` 0)xxx
      )xxx }

1
1. r : CRng
2. h : ℕ+ ⟶ ℕ+ ⟶ |r|
3. b : bag(Prime)
4. IntDeq ∈ EqDecider(Prime)
⊢ Σ(p∈bag-partitions(IntDeq;b)). h[Π(fst(p));Π(snd(p))]
= Σ(i∈[1, Π(b) + 1)). if (Π(b) rem i =z 0) then h[i;Π(b) ÷ i] else 0 fi 
∈ |r|

---

Latex:

---

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


By

---

Latex:
xxx(Unfold  `gen-divisors-sum`  0
        THEN  xxx(Auto
                          THEN  (Assert  IntDeq  \mmember{}  EqDecider(Prime)  BY
                                                  ((DoSubsume  THEN  Auto)  THEN  BLemma  `strong-subtype-deq-subtype`  THEN  Auto))
                          THEN  RepUR  ``let``  0)xxx
        )xxx

---

Home Index