---

Step * 1 1 1 1 2 of Lemma canon-bnd_wf


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)|)
5. ¬(n = 1 ∈ ℤ)
⊢ |x n| ≤ (n * (|x 1| + 3))
BY
{ ((RWO "-2" 0 THENA Auto)
   THEN (RWO "-3" 0 THENA Auto)
   THEN (RWO "absval_mul" 0 THENA Auto)
   THEN (Subst' |n| ~ n 0 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)|)
5. ¬(n = 1 ∈ ℤ)
⊢ ((2 + (2 * n)) + (n * |x 1|)) ≤ (n * (|x 1| + 3))

---

Latex:

---

Latex:

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


By

---

Latex:
((RWO  "-2"  0  THENA  Auto)
  THEN  (RWO  "-3"  0  THENA  Auto)
  THEN  (RWO  "absval\_mul"  0  THENA  Auto)
  THEN  (Subst'  |n|  \msim{}  n  0  THENA  Auto))

---

Home Index