---

Step * 1 2 of Lemma triangular-num-alt


1. k : ℕ@i
2. r : ℕ2@i
3. ¬(r = 0 ∈ ℤ)
⊢ ((((k * 2) + r) * (((k * 2) + r) + 1)) ÷ 2) = ((k + r) * ((2 * k) + 1)) ∈ ℤ
BY
{ ((Subst ⌜r ~ 1⌝ 0⋅ THEN Auto') THEN RW IntNormC 0 THEN Auto) }

1
1. k : ℕ@i
2. r : ℕ2@i
3. ¬(r = 0 ∈ ℤ)
⊢ ((2 + (6 * k) + (4 * k * k)) ÷ 2) = (1 + (3 * k) + (2 * k * k)) ∈ ℤ

---

Latex:

---

Latex:

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


By

---

Latex:
((Subst  \mkleeneopen{}r  \msim{}  1\mkleeneclose{}  0\mcdot{}  THEN  Auto')  THEN  RW  IntNormC  0  THEN  Auto)

---

Home Index