Step
*
of Lemma
divisors-sum_wf
∀[n:ℕ+]. ∀[f:ℕ+n + 1 ⟶ ℤ].  (Σ i|n. f[i]  ∈ ℤ)
BY
{ xxxProveWfLemmaxxx }
Latex:
Latex:
\mforall{}[n:\mBbbN{}\msupplus{}].  \mforall{}[f:\mBbbN{}\msupplus{}n  +  1  {}\mrightarrow{}  \mBbbZ{}].    (\mSigma{}  i|n.  f[i]    \mmember{}  \mBbbZ{})
By
Latex:
xxxProveWfLemmaxxx
Home
Index