---

Step * of Lemma rnonneg-rmul

∀x,y:ℝ.  (rnonneg(x) ⇒ rnonneg(y) ⇒ rnonneg(x * y))
BY
{ (RepeatFor 2 ((D 0 THENA Auto))
   THEN RWO "rnonneg-iff" 0
   THEN Auto
   THEN Unfold `rmul` 0
   THEN RepeatFor 2 ((CallByValueReduce 0 THENA Auto))
   THEN (Assert 0 < (2 * imax(canonical-bound(x);canonical-bound(y))) + 1 BY
               ((RWO "imax_unfold" 0 THENA Auto) THEN AutoSplit THEN GenConclAtAddr [2;1;2] THEN D -2 THEN Auto'))
   THEN (RWO "accelerate-bdd-diff" 0 THENA Auto)
   THEN Thin (-1)
   THEN All (Unfold `rnonneg2`)
   THEN RepUR ``reg-seq-mul`` 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)) ÷ 2 * m)))

---

Latex:

---

Latex:
\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  Unfold  `rmul`  0
  THEN  RepeatFor  2  ((CallByValueReduce  0  THENA  Auto))
  THEN  (Assert  0  <  (2  *  imax(canonical-bound(x);canonical-bound(y)))  +  1  BY
                          ((RWO  "imax\_unfold"  0  THENA  Auto)
                            THEN  AutoSplit
                            THEN  GenConclAtAddr  [2;1;2]
                            THEN  D  -2
                            THEN  Auto'))
  THEN  (RWO  "accelerate-bdd-diff"  0  THENA  Auto)
  THEN  Thin  (-1)
  THEN  All  (Unfold  `rnonneg2`)
  THEN  RepUR  ``reg-seq-mul``  0
  THEN  Auto)

---

Home Index