---

Step * 2 1 1 1 1 1 1 of Lemma infinitesmal-zero


1. x : ℝ
2. k : ℕ+
3. rnonneg2(reg-seq-add(r1;-(reg-seq-mul(r(k);|x|))))
4. r(k) ≠ r0
⊢ rnonneg2(λn.((2 * n) - k * |x n|))
BY
{ (RepUR ``reg-seq-add int-to-real rminus reg-seq-mul rabs rmax`` (-2)
   THEN RepeatFor 2 (ParallelOp -2)
   THEN RepeatFor 2 (ParallelLast)
   THEN All Reduce
   THEN NthHypEq (-1)
   THEN RepeatFor 2 ((EqCD THEN Auto))) }

1
.....subterm..... T:t
2:n
1. x : ℝ
2. k : ℕ+
3. ∀n:ℕ+. ∃N:ℕ+. ∀m:{N...}. (((-2) * m) ≤ (n * ((2 * m * 1) + (-(((2 * m * k) * |x m|) ÷ 2 * m)))))
4. r(k) ≠ r0
5. n : ℕ+
6. N : ℕ+
7. ∀m:{N...}. (((-2) * m) ≤ (n * ((2 * m * 1) + (-(((2 * m * k) * |x m|) ÷ 2 * m)))))
8. m : {N...}
9. ((-2) * m) ≤ (n * ((2 * m * 1) + (-(((2 * m * k) * |x m|) ÷ 2 * m))))
⊢ ((2 * m) - k * |x m|) = ((2 * m * 1) + (-(((2 * m * k) * |x m|) ÷ 2 * m))) ∈ ℤ

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  k  :  \mBbbN{}\msupplus{}
3.  rnonneg2(reg-seq-add(r1;-(reg-seq-mul(r(k);|x|))))
4.  r(k)  \mneq{}  r0
\mvdash{}  rnonneg2(\mlambda{}n.((2  *  n)  -  k  *  |x  n|))


By

---

Latex:
(RepUR  ``reg-seq-add  int-to-real  rminus  reg-seq-mul  rabs  rmax``  (-2)
  THEN  RepeatFor  2  (ParallelOp  -2)
  THEN  RepeatFor  2  (ParallelLast)
  THEN  All  Reduce
  THEN  NthHypEq  (-1)
  THEN  RepeatFor  2  ((EqCD  THEN  Auto)))

---

Home Index