---

Step * 1 2 1 of Lemma triangular-num-alt


1. k : ℕ@i
2. r : ℕ2@i
3. ¬(r = 0 ∈ ℤ)
⊢ ((2 + (6 * k) + (4 * k * k)) ÷ 2) = (1 + (3 * k) + (2 * k * k)) ∈ ℤ
BY
{ ((InstLemma `div-cancel` [⌜1 + (3 * k) + (2 * k * k)⌝;⌜2⌝]⋅ THENA Auto) THEN RevHypSubst (-1) 0⋅ THEN EqCD THEN Auto)
⋅ }

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}@i
2.  r  :  \mBbbN{}2@i
3.  \mneg{}(r  =  0)
\mvdash{}  ((2  +  (6  *  k)  +  (4  *  k  *  k))  \mdiv{}  2)  =  (1  +  (3  *  k)  +  (2  *  k  *  k))


By

---

Latex:
((InstLemma  `div-cancel`  [\mkleeneopen{}1  +  (3  *  k)  +  (2  *  k  *  k)\mkleeneclose{};\mkleeneopen{}2\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RevHypSubst  (-1)  0\mcdot{}
  THEN  EqCD
  THEN  Auto)\mcdot{}

---

Home Index