---

Step * of Lemma rnonneg2_functionality

∀x,y:ℕ+ ⟶ ℤ.  (bdd-diff(x;y) ⇒ (rnonneg2(x) ⇐⇒ rnonneg2(y)))
BY
{ (Assert ⌜∀x,y:ℕ+ ⟶ ℤ.  (bdd-diff(x;y) ⇒ rnonneg2(x) ⇒ rnonneg2(y))⌝⋅
   THEN Auto
   THEN Try (((InstHyp [⌜y⌝;⌜x⌝] 1⋅ THEN Auto) THEN RelRST THEN Auto))
   THEN D -2
   THEN All (Unfold `rnonneg2`)
   THEN Auto) }

1
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 : ℕ+
⊢ ∃N:ℕ+. ∀m:{N...}. (((-2) * m) ≤ (n * (y m)))

---

Latex:

---

Latex:
\mforall{}x,y:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}.    (bdd-diff(x;y)  {}\mRightarrow{}  (rnonneg2(x)  \mLeftarrow{}{}\mRightarrow{}  rnonneg2(y)))


By

---

Latex:
(Assert  \mkleeneopen{}\mforall{}x,y:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}.    (bdd-diff(x;y)  {}\mRightarrow{}  rnonneg2(x)  {}\mRightarrow{}  rnonneg2(y))\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  Try  (((InstHyp  [\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]  1\mcdot{}  THEN  Auto)  THEN  RelRST  THEN  Auto))
  THEN  D  -2
  THEN  All  (Unfold  `rnonneg2`)
  THEN  Auto)

---

Home Index