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