---

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


1. r : CRng
2. h : ℕ+ ⟶ ℕ+ ⟶ |r|
3. b : bag(Prime)
4. IntDeq ∈ EqDecider(Prime)
5. n : ℕ+
6. Π(b) = n ∈ ℕ+
7. [1, n + 1) ∈ bag(ℕ+n + 1)
8. ∀[R:Type]. ∀[add:R ⟶ R ⟶ R]. ∀[zero:R]. ∀[b:bag(ℕ+n + 1)]. ∀[p:ℕ+n + 1 ⟶ 𝔹]. ∀[f:ℕ+n + 1 ⟶ R].
     Σ(x∈[x∈b|p[x]]). f[x] = Σ(x∈b). if p[x] then f[x] else zero fi  ∈ R supposing IsMonoid(R;add;zero) ∧ Comm(R;add)
⊢ Σ(x∈[i∈[1, n + 1)|(n rem i =z 0)]). h[x;n ÷ x] = Σ(i∈[1, n + 1)). if (n rem i =z 0) then h[i;n ÷ i] else 0 fi  ∈ |r|
BY
{ xxx(RWO "-1" 0 THENA (Auto THEN RepeatFor 2 ((D 0 THEN Reduce 0 THEN Auto))))xxx }

---

Latex:

---

Latex:

1.  r  :  CRng
2.  h  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbN{}\msupplus{}  {}\mrightarrow{}  |r|
3.  b  :  bag(Prime)
4.  IntDeq  \mmember{}  EqDecider(Prime)
5.  n  :  \mBbbN{}\msupplus{}
6.  \mPi{}(b)  =  n
7.  [1,  n  +  1)  \mmember{}  bag(\mBbbN{}\msupplus{}n  +  1)
8.  \mforall{}[R:Type].  \mforall{}[add:R  {}\mrightarrow{}  R  {}\mrightarrow{}  R].  \mforall{}[zero:R].  \mforall{}[b:bag(\mBbbN{}\msupplus{}n  +  1)].  \mforall{}[p:\mBbbN{}\msupplus{}n  +  1  {}\mrightarrow{}  \mBbbB{}].
      \mforall{}[f:\mBbbN{}\msupplus{}n  +  1  {}\mrightarrow{}  R].
          \mSigma{}(x\mmember{}[x\mmember{}b|p[x]]).  f[x]  =  \mSigma{}(x\mmember{}b).  if  p[x]  then  f[x]  else  zero  fi   
          supposing  IsMonoid(R;add;zero)  \mwedge{}  Comm(R;add)
\mvdash{}  \mSigma{}(x\mmember{}[i\mmember{}[1,  n  +  1)|(n  rem  i  =\msubz{}  0)]).  h[x;n  \mdiv{}  x]
=  \mSigma{}(i\mmember{}[1,  n  +  1)).  if  (n  rem  i  =\msubz{}  0)  then  h[i;n  \mdiv{}  i]  else  0  fi 


By

---

Latex:
xxx(RWO  "-1"  0  THENA  (Auto  THEN  RepeatFor  2  ((D  0  THEN  Reduce  0  THEN  Auto))))xxx

---

Home Index