---

Step * 1 2 2 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 ∈ ℕ+
⊢ Σ(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((Assert [1, n + 1) ∈ bag(ℕ+n + 1) BY Auto) THEN (InstLemma `bag-summation-filter` [⌜ℕ+n + 1⌝]⋅ THENA Auto))xxx }

1
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|

---

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
\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((Assert  [1,  n  +  1)  \mmember{}  bag(\mBbbN{}\msupplus{}n  +  1)  BY
                      Auto)
        THEN  (InstLemma  `bag-summation-filter`  [\mkleeneopen{}\mBbbN{}\msupplus{}n  +  1\mkleeneclose{}]\mcdot{}  THENA  Auto)
        )xxx

---

Home Index