---

Step * 1 1 of Lemma real-approx


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))|)))
BY
{ RepUR ``rnonneg2 reg-seq-add rminus rabs rmax reg-seq-mul int-to-real`` 0 }

1
1. x : ℝ
2. n : ℕ+
3. r(2 * n) = |r(2 * n)|
⊢ ∀n@0:ℕ+
    ∃N:ℕ+
     ∀m:{N...}. (((-2) * m) ≤ (n@0 * ((2 * m * 2) + (-|(-(2 * m * (x n))) + (((2 * m * 2 * n) * (x m)) ÷ 2 * m)|))))

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  n  :  \mBbbN{}\msupplus{}
3.  r(2  *  n)  =  |r(2  *  n)|
\mvdash{}  rnonneg2(reg-seq-add(r(2);-(|reg-seq-add(-(r(x  n));reg-seq-mul(r(2  *  n);x))|)))


By

---

Latex:
RepUR  ``rnonneg2  reg-seq-add  rminus  rabs  rmax  reg-seq-mul  int-to-real``  0

---

Home Index