---

Step * 1 of Lemma rpositive2_functionality


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))))
BY
{ (D 3 THEN ((With ⌜(B + 1) * n⌝ (D 0)⋅ THENA Auto) THEN RepeatFor 2 (ParallelLast) THEN Auto')⋅) }

1
.....antecedent..... 
1. x : ℕ+ ⟶ ℤ@i
2. y : ℕ+ ⟶ ℤ@i
3. B : ℕ@i
4. ∀n:ℕ+. (|(x n) - y n| ≤ B)@i
5. n : ℕ+@i
6. ∀m:ℕ+. ((n ≤ m) ⇒ (m ≤ (n * (x m))))@i
7. m : ℕ+@i
8. ((B + 1) * n) ≤ m@i
⊢ n ≤ m

2
1. x : ℕ+ ⟶ ℤ@i
2. y : ℕ+ ⟶ ℤ@i
3. B : ℕ@i
4. ∀n:ℕ+. (|(x n) - y n| ≤ B)@i
5. n : ℕ+@i
6. ∀m:ℕ+. ((n ≤ m) ⇒ (m ≤ (n * (x m))))@i
7. m : ℕ+@i
8. ((B + 1) * n) ≤ m@i
9. m ≤ (n * (x m))
⊢ m ≤ (((B + 1) * n) * (y m))

---

Latex:

---

Latex:

1.  x  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}@i
2.  y  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}@i
3.  bdd-diff(x;y)@i
4.  n  :  \mBbbN{}\msupplus{}@i
5.  \mforall{}m:\mBbbN{}\msupplus{}.  ((n  \mleq{}  m)  {}\mRightarrow{}  (m  \mleq{}  (n  *  (x  m))))@i
\mvdash{}  \mexists{}n:\mBbbN{}\msupplus{}.  \mforall{}m:\mBbbN{}\msupplus{}.  ((n  \mleq{}  m)  {}\mRightarrow{}  (m  \mleq{}  (n  *  (y  m))))


By

---

Latex:
(D  3  THEN  ((With  \mkleeneopen{}(B  +  1)  *  n\mkleeneclose{}  (D  0)\mcdot{}  THENA  Auto)  THEN  RepeatFor  2  (ParallelLast)  THEN  Auto')\mcdot{})

---

Home Index