---

Step * of Lemma rpositive-radd2

∀x,y:ℝ.  (rpositive(x) ⇒ rnonneg(y) ⇒ rpositive(x + y))
BY
{ (RepeatFor 2 ((D 0 THENA Auto))
   THEN RWO "rnonneg-iff rpositive-iff" 0
   THEN Auto
   THEN RepUR ``radd`` 0
   THEN (RWO "accelerate-bdd-diff" 0 THENA Auto)
   THEN (RWO "reg-seq-list-add-as-l_sum" 0 THENA Auto)
   THEN All (Unfolds ``rnonneg2 rpositive2``)
   THEN Reduce 0
   THEN Auto
   THEN ExRepD
   THEN (InstHyp [⌜3 * n⌝] (-1)⋅ THENA Auto)
   THEN ExRepD) }

1
1. x : ℝ@i
2. y : ℝ@i
3. n : ℕ+@i
4. ∀m:ℕ+. ((n ≤ m) ⇒ (m ≤ (n * (x m))))@i
5. ∀n:ℕ+. ∃N:ℕ+. ∀m:{N...}. (((-2) * m) ≤ (n * (y m)))@i
6. N : ℕ+
7. ∀m:{N...}. (((-2) * m) ≤ ((3 * n) * (y m)))
⊢ ∃n:ℕ+. ∀m:ℕ+. ((n ≤ m) ⇒ (m ≤ (n * ((x m) + (y m) + 0))))

---

Latex:

---

Latex:
\mforall{}x,y:\mBbbR{}.    (rpositive(x)  {}\mRightarrow{}  rnonneg(y)  {}\mRightarrow{}  rpositive(x  +  y))


By

---

Latex:
(RepeatFor  2  ((D  0  THENA  Auto))
  THEN  RWO  "rnonneg-iff  rpositive-iff"  0
  THEN  Auto
  THEN  RepUR  ``radd``  0
  THEN  (RWO  "accelerate-bdd-diff"  0  THENA  Auto)
  THEN  (RWO  "reg-seq-list-add-as-l\_sum"  0  THENA  Auto)
  THEN  All  (Unfolds  ``rnonneg2  rpositive2``)
  THEN  Reduce  0
  THEN  Auto
  THEN  ExRepD
  THEN  (InstHyp  [\mkleeneopen{}3  *  n\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
  THEN  ExRepD)

---

Home Index