---

Step * 1 of Lemma rnonneg-int


1. n : ℤ
2. ∀n@0:ℕ+. ((-2) ≤ (2 * n@0 * n))
⊢ 0 ≤ n
BY
{ (With ⌜2⌝ (D 2)⋅ THEN Auto') }

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  \mforall{}n@0:\mBbbN{}\msupplus{}.  ((-2)  \mleq{}  (2  *  n@0  *  n))
\mvdash{}  0  \mleq{}  n


By

---

Latex:
(With  \mkleeneopen{}2\mkleeneclose{}  (D  2)\mcdot{}  THEN  Auto')

---

Home Index