---

Step * 1 1 1 of Lemma rpositive-iff


1. x : ℕ+ ⟶ ℤ
2. ∀n,m:ℕ+.  (|(m * (x n)) - n * (x m)| ≤ ((2 * 1) * (n + m)))
3. n : ℕ+
4. 4 < x n
5. m : ℕ+
6. n ≤ m
7. ∀m:ℕ+. ((n ≤ m) ⇒ (m ≤ (n * |x m|)))
8. m ≤ (n * (-(x m)))
9. ¬0 < x m
10. |(m * (x n)) - n * (x m)| ≤ ((2 * 1) * (n + m))
⊢ False
BY
{ ((InstLemma `mul_preserves_le` [⌜x m⌝;⌜0⌝;⌜n⌝]⋅ THENA Auto)
   THEN (InstLemma `mul_preserves_lt` [⌜4⌝;⌜x n⌝;⌜m⌝]⋅ THENA Auto)
   THEN RWO "absval_pos" (-3)⋅
   THEN Auto) }

---

Latex:

---

Latex:

1.  x  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}
2.  \mforall{}n,m:\mBbbN{}\msupplus{}.    (|(m  *  (x  n))  -  n  *  (x  m)|  \mleq{}  ((2  *  1)  *  (n  +  m)))
3.  n  :  \mBbbN{}\msupplus{}
4.  4  <  x  n
5.  m  :  \mBbbN{}\msupplus{}
6.  n  \mleq{}  m
7.  \mforall{}m:\mBbbN{}\msupplus{}.  ((n  \mleq{}  m)  {}\mRightarrow{}  (m  \mleq{}  (n  *  |x  m|)))
8.  m  \mleq{}  (n  *  (-(x  m)))
9.  \mneg{}0  <  x  m
10.  |(m  *  (x  n))  -  n  *  (x  m)|  \mleq{}  ((2  *  1)  *  (n  +  m))
\mvdash{}  False


By

---

Latex:
((InstLemma  `mul\_preserves\_le`  [\mkleeneopen{}x  m\mkleeneclose{};\mkleeneopen{}0\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `mul\_preserves\_lt`  [\mkleeneopen{}4\mkleeneclose{};\mkleeneopen{}x  n\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RWO  "absval\_pos"  (-3)\mcdot{}
  THEN  Auto)

---

Home Index