---

Step * 1 1 of Lemma rnonneg2_functionality

.....wf..... 
1. x : ℕ+ ⟶ ℤ
2. y : ℕ+ ⟶ ℤ
3. B : ℕ
4. ∀n:ℕ+. (|(x n) - y n| ≤ B)
5. ∀n:ℕ+. ∃N:ℕ+. ∀m:{N...}. (((-2) * m) ≤ (n * (x m)))
6. n : ℕ+
7. N : ℕ+
8. ∀m:{N...}. (((-2) * m) ≤ ((2 * n) * (x m)))
⊢ imax(N;n * B) ∈ ℕ+
BY
{ (Subst' imax(N;n * B) ~ imax(n * B;N) 0 THEN Auto) }

---

Latex:

---

Latex:
.....wf..... 
1.  x  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}
2.  y  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}
3.  B  :  \mBbbN{}
4.  \mforall{}n:\mBbbN{}\msupplus{}.  (|(x  n)  -  y  n|  \mleq{}  B)
5.  \mforall{}n:\mBbbN{}\msupplus{}.  \mexists{}N:\mBbbN{}\msupplus{}.  \mforall{}m:\{N...\}.  (((-2)  *  m)  \mleq{}  (n  *  (x  m)))
6.  n  :  \mBbbN{}\msupplus{}
7.  N  :  \mBbbN{}\msupplus{}
8.  \mforall{}m:\{N...\}.  (((-2)  *  m)  \mleq{}  ((2  *  n)  *  (x  m)))
\mvdash{}  imax(N;n  *  B)  \mmember{}  \mBbbN{}\msupplus{}


By

---

Latex:
(Subst'  imax(N;n  *  B)  \msim{}  imax(n  *  B;N)  0  THEN  Auto)

---

Home Index