---

Step * of Lemma rpositive-rmul

∀x,y:ℝ.  (rpositive(x) ⇒ rpositive(y) ⇒ rpositive(x * y))
BY
{ (RepeatFor 2 ((D 0 THENA Auto))
   THEN RWO "rpositive-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 `rpositive2`)
   THEN ExRepD) }

1
1. x : ℝ
2. y : ℝ
3. n1 : ℕ+
4. ∀m:ℕ+. ((n1 ≤ m) ⇒ (m ≤ (n1 * (x m))))
5. n : ℕ+
6. ∀m:ℕ+. ((n ≤ m) ⇒ (m ≤ (n * (y m))))
⊢ ∃n:ℕ+. ∀m:ℕ+. ((n ≤ m) ⇒ (m ≤ (n * (reg-seq-mul(x;y) m))))

---

Latex:

---

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


By

---

Latex:
(RepeatFor  2  ((D  0  THENA  Auto))
  THEN  RWO  "rpositive-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  `rpositive2`)
  THEN  ExRepD)

---

Home Index