---

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


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)
∈ ℤ
BY
{ xxx((RWO "bag-summation-from-upto" 0 THENA Auto) THEN EqCD THEN Auto)xxx }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}\msupplus{}
2.  f  :  \mBbbN{}\msupplus{}n  +  1  {}\mrightarrow{}  \mBbbZ{}
3.  [1,  n  +  1)  \mmember{}  bag(\mBbbN{}\msupplus{}n  +  1)
\mvdash{}  \mSigma{}(i\mmember{}[1,  n  +  1)).  if  (n  rem  i  =\msubz{}  0)  then  f[i]  else  0  fi 
=  \mSigma{}(if  (n  rem  i  +  1  =\msubz{}  0)  then  f[i  +  1]  else  0  fi    |  i  <  n)


By

---

Latex:
xxx((RWO  "bag-summation-from-upto"  0  THENA  Auto)  THEN  EqCD  THEN  Auto)xxx

---

Home Index