---

Step * of Lemma not-rpositive

∀[x:ℝ]. rnonneg(-(x)) supposing ¬rpositive(x)
BY
{ (Auto THEN (Assert ∀n:ℕ+. ((x n) ≤ 4) BY (Auto THEN SupposeNot THEN Auto THEN D 2 THEN With ⌜n⌝ (D 0)⋅ THEN Auto))) }

1
1. x : ℝ
2. ¬rpositive(x)
3. ∀n:ℕ+. ((x n) ≤ 4)
⊢ rnonneg(-(x))

---

Latex:

---

Latex:
\mforall{}[x:\mBbbR{}].  rnonneg(-(x))  supposing  \mneg{}rpositive(x)


By

---

Latex:
(Auto
  THEN  (Assert  \mforall{}n:\mBbbN{}\msupplus{}.  ((x  n)  \mleq{}  4)  BY
                          (Auto  THEN  SupposeNot  THEN  Auto  THEN  D  2  THEN  With  \mkleeneopen{}n\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto))
  )

---

Home Index