---

Step * 1 1 1 of Lemma canon-bnd_wf


1. x : ℕ+ ⟶ ℤ
2. n : ℕ+
3. |(1 * (x n)) - n * (x 1)| ≤ (2 * (n + 1))
⊢ |x n| ≤ (n * (|x 1| + 3))
BY
{ ((RW IntNormC (-1) THENA Auto)
   THEN (InstLemma `int-triangle-inequality` [⌜n * (x 1)⌝;⌜(1 * (x n)) - n * (x 1)⌝]⋅ THENA Auto)
   THEN (RW IntNormC (-1) THENA Auto)) }

1
1. x : ℕ+ ⟶ ℤ
2. n : ℕ+
3. |(x n) + ((-1) * n * (x 1))| ≤ (2 + (2 * n))
4. |x n| ≤ (|(x n) + ((-1) * n * (x 1))| + |n * (x 1)|)
⊢ |x n| ≤ (n * (|x 1| + 3))

---

Latex:

---

Latex:

1.  x  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}
2.  n  :  \mBbbN{}\msupplus{}
3.  |(1  *  (x  n))  -  n  *  (x  1)|  \mleq{}  (2  *  (n  +  1))
\mvdash{}  |x  n|  \mleq{}  (n  *  (|x  1|  +  3))


By

---

Latex:
((RW  IntNormC  (-1)  THENA  Auto)
  THEN  (InstLemma  `int-triangle-inequality`  [\mkleeneopen{}n  *  (x  1)\mkleeneclose{};\mkleeneopen{}(1  *  (x  n))  -  n  *  (x  1)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RW  IntNormC  (-1)  THENA  Auto))

---

Home Index