---

Step * of Lemma rnonneg-radd

No Annotations
∀x,y:ℝ.  (rnonneg(x) ⇒ rnonneg(y) ⇒ rnonneg(x + y))
BY
{ (RepeatFor 2 ((D 0 THENA Auto))
   THEN RWO "rnonneg-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 (Unfold `rnonneg2`)
   THEN Reduce 0
   THEN Auto) }

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

---

Latex:

---

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


By

---

Latex:
(RepeatFor  2  ((D  0  THENA  Auto))
  THEN  RWO  "rnonneg-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  (Unfold  `rnonneg2`)
  THEN  Reduce  0
  THEN  Auto)

---

Home Index