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 -2
   THEN All (Unfold `rnonneg2`)
   THEN Auto) }

1
1. : ℕ+ ⟶ ℤ
2. : ℕ+ ⟶ ℤ
3. : ℕ
4. ∀n:ℕ+(|(x n) n| ≤ B)
5. ∀n:ℕ+. ∃N:ℕ+. ∀m:{N...}. (((-2) m) ≤ (n (x m)))
6. : ℕ+
⊢ ∃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