---

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

.....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))) ∈ ℤ
BY
{ ((Subst' (2 * m * k) * |x m| ~ (k * |x m|) * 2 * m 0 THENA Auto) THEN RWO "div-cancel" 0 THEN Auto) }

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
1.  x  :  \mBbbR{}
2.  k  :  \mBbbN{}\msupplus{}
3.  \mforall{}n:\mBbbN{}\msupplus{}.  \mexists{}N:\mBbbN{}\msupplus{}.  \mforall{}m:\{N...\}.  (((-2)  *  m)  \mleq{}  (n  *  ((2  *  m  *  1)  +  (-(((2  *  m  *  k)  *  |x  m|)  \mdiv{}  2  *  m)))))
4.  r(k)  \mneq{}  r0
5.  n  :  \mBbbN{}\msupplus{}
6.  N  :  \mBbbN{}\msupplus{}
7.  \mforall{}m:\{N...\}.  (((-2)  *  m)  \mleq{}  (n  *  ((2  *  m  *  1)  +  (-(((2  *  m  *  k)  *  |x  m|)  \mdiv{}  2  *  m)))))
8.  m  :  \{N...\}
9.  ((-2)  *  m)  \mleq{}  (n  *  ((2  *  m  *  1)  +  (-(((2  *  m  *  k)  *  |x  m|)  \mdiv{}  2  *  m))))
\mvdash{}  ((2  *  m)  -  k  *  |x  m|)  =  ((2  *  m  *  1)  +  (-(((2  *  m  *  k)  *  |x  m|)  \mdiv{}  2  *  m)))


By

---

Latex:
((Subst'  (2  *  m  *  k)  *  |x  m|  \msim{}  (k  *  |x  m|)  *  2  *  m  0  THENA  Auto)  THEN  RWO  "div-cancel"  0  THEN  Auto)

---

Home Index