---

Step * of Lemma rpositive2_functionality

∀x,y:ℕ+ ⟶ ℤ.  (bdd-diff(x;y) ⇒ (rpositive2(x) ⇐⇒ rpositive2(y)))
BY
{ (Assert ⌜∀x,y:ℕ+ ⟶ ℤ.  (bdd-diff(x;y) ⇒ rpositive2(x) ⇒ rpositive2(y))⌝⋅
   THEN Auto
   THEN Try ((InstHyp [⌜y⌝;⌜x⌝] 1⋅ THEN Auto THEN RelRST THEN Auto))
   THEN ParallelLast
   THEN ExRepD) }

1
1. x : ℕ+ ⟶ ℤ@i
2. y : ℕ+ ⟶ ℤ@i
3. bdd-diff(x;y)@i
4. n : ℕ+@i
5. ∀m:ℕ+. ((n ≤ m) ⇒ (m ≤ (n * (x m))))@i
⊢ ∃n:ℕ+. ∀m:ℕ+. ((n ≤ m) ⇒ (m ≤ (n * (y m))))

---

Latex:

---

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


By

---

Latex:
(Assert  \mkleeneopen{}\mforall{}x,y:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}.    (bdd-diff(x;y)  {}\mRightarrow{}  rpositive2(x)  {}\mRightarrow{}  rpositive2(y))\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  Try  ((InstHyp  [\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]  1\mcdot{}  THEN  Auto  THEN  RelRST  THEN  Auto))
  THEN  ParallelLast
  THEN  ExRepD)

---

Home Index