---

Step * 1 of Lemma real-approx


1. x : ℝ
2. n : ℕ+
3. r(2 * n) = |r(2 * n)|
⊢ |-(r(x n)) + (r(2 * n) * x)| ≤ r(2)
BY
{ (TACTIC:Unfold `rleq` 0
   THEN (BLemma `rnonneg-iff` THENA Auto)
   THEN Unfold `rsub` 0
   THEN (RWO "radd-bdd-diff" 0 THENA Auto)
   THEN Fold `reg-seq-add` 0
   THEN (RWO "radd-bdd-diff" 0 THENA (Try (Complete (Auto)) THEN RepUR ``rminus rabs rmax`` 0 THEN Auto))
   THEN Try (Fold `reg-seq-add` 0)
   THEN (RWO "rmul-bdd-diff-reg-seq-mul" 0
         THENA (Try (Complete (Auto)) THEN Try ((RepUR ``rminus rabs rmax`` 0 THEN Complete (Auto))⋅))
         )) }

1
1. x : ℝ
2. n : ℕ+
3. r(2 * n) = |r(2 * n)|
⊢ rnonneg2(reg-seq-add(r(2);-(|reg-seq-add(-(r(x n));reg-seq-mul(r(2 * n);x))|)))

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  n  :  \mBbbN{}\msupplus{}
3.  r(2  *  n)  =  |r(2  *  n)|
\mvdash{}  |-(r(x  n))  +  (r(2  *  n)  *  x)|  \mleq{}  r(2)


By

---

Latex:
(TACTIC:Unfold  `rleq`  0
  THEN  (BLemma  `rnonneg-iff`  THENA  Auto)
  THEN  Unfold  `rsub`  0
  THEN  (RWO  "radd-bdd-diff"  0  THENA  Auto)
  THEN  Fold  `reg-seq-add`  0
  THEN  (RWO  "radd-bdd-diff"  0
              THENA  (Try  (Complete  (Auto))  THEN  RepUR  ``rminus  rabs  rmax``  0  THEN  Auto)
              )
  THEN  Try  (Fold  `reg-seq-add`  0)
  THEN  (RWO  "rmul-bdd-diff-reg-seq-mul"  0
              THENA  (Try  (Complete  (Auto))  THEN  Try  ((RepUR  ``rminus  rabs  rmax``  0  THEN  Complete  (Auto))\mcdot{}))
              ))

---

Home Index