---

Step * 2 of Lemma rpositive-iff


1. [x] : ℝ
2. n : ℕ+
3. ∀m:ℕ+. ((n ≤ m) ⇒ (m ≤ (n * (x m))))
⊢ rpositive(x)
BY
{ (With ⌜5 * n⌝ (D 0)⋅
   THEN Auto
   THEN (InstHyp [⌜5 * n⌝] (-1)⋅ THENA Auto)
   THEN Using [`n',⌜n⌝] (BLemma `mul_cancel_in_lt`)⋅
   THEN Auto) }

---

Latex:

---

Latex:

1.  [x]  :  \mBbbR{}
2.  n  :  \mBbbN{}\msupplus{}
3.  \mforall{}m:\mBbbN{}\msupplus{}.  ((n  \mleq{}  m)  {}\mRightarrow{}  (m  \mleq{}  (n  *  (x  m))))
\mvdash{}  rpositive(x)


By

---

Latex:
(With  \mkleeneopen{}5  *  n\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Auto
  THEN  (InstHyp  [\mkleeneopen{}5  *  n\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
  THEN  Using  [`n',\mkleeneopen{}n\mkleeneclose{}]  (BLemma  `mul\_cancel\_in\_lt`)\mcdot{}
  THEN  Auto)

---

Home Index