---

Step * of Lemma sum_arith

∀[n:ℕ]. ∀[a,b:ℤ].  (Σ(a + (b * i) | i < n) = ((n * (a + a + (b * (n - 1)))) ÷ 2) ∈ ℤ)
BY
{ ((Auto THEN InstLemma `sum_arith1` [⌜n⌝;⌜a⌝;⌜b⌝]) THENA Auto) }

1
1. n : ℕ
2. a : ℤ
3. b : ℤ
4. (Σ(a + (b * i) | i < n) * 2) = (n * (a + a + (b * (n - 1)))) ∈ ℤ
⊢ Σ(a + (b * i) | i < n) = ((n * (a + a + (b * (n - 1)))) ÷ 2) ∈ ℤ

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[a,b:\mBbbZ{}].    (\mSigma{}(a  +  (b  *  i)  |  i  <  n)  =  ((n  *  (a  +  a  +  (b  *  (n  -  1))))  \mdiv{}  2))


By

---

Latex:
((Auto  THEN  InstLemma  `sum\_arith1`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}])  THENA  Auto)

---

Home Index