---

Step * of Lemma gen-divisors-sum-int-ring

∀[n:ℕ+]. ∀[f:ℕ+n + 1 ⟶ ℤ].  (Σ i|n. f[i] = Σ i|n. f[i]  ∈ ℤ)
BY
{ xxx(Auto THEN RepUR ``gen-divisors-sum divisors-sum`` 0 THEN (Assert [1, n + 1) ∈ bag(ℕ+n + 1) BY Auto))xxx }

1
1. n : ℕ+
2. f : ℕ+n + 1 ⟶ ℤ
3. [1, n + 1) ∈ bag(ℕ+n + 1)
⊢ Σ(i∈[1, n + 1)). if (n rem i =z 0) then f[i] else 0 fi 
= Σ(if (n rem i + 1 =z 0) then f[i + 1] else 0 fi  | i < n)
∈ ℤ

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}\msupplus{}].  \mforall{}[f:\mBbbN{}\msupplus{}n  +  1  {}\mrightarrow{}  \mBbbZ{}].    (\mSigma{}  i|n.  f[i]  =  \mSigma{}  i|n.  f[i]  )


By

---

Latex:
xxx(Auto
        THEN  RepUR  ``gen-divisors-sum  divisors-sum``  0
        THEN  (Assert  [1,  n  +  1)  \mmember{}  bag(\mBbbN{}\msupplus{}n  +  1)  BY
                                Auto))xxx

---

Home Index