---

Step * 1 of Lemma rsum-triangle-inequality1


1. n : ℤ
2. m : ℤ
3. x : {n..m + 1-} ⟶ ℝ
4. y : {n..m + 1-} ⟶ ℝ
5. i : ℤ
6. n ≤ i
7. i ≤ m
⊢ |x[i]| ≤ (|x[i] + y[i]| + |y[i]|)
BY
{ (Assert |y[i]| = |-(y[i])| BY
         Auto) }

1
1. n : ℤ
2. m : ℤ
3. x : {n..m + 1-} ⟶ ℝ
4. y : {n..m + 1-} ⟶ ℝ
5. i : ℤ
6. n ≤ i
7. i ≤ m
8. |y[i]| = |-(y[i])|
⊢ |x[i]| ≤ (|x[i] + y[i]| + |y[i]|)

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  m  :  \mBbbZ{}
3.  x  :  \{n..m  +  1\msupminus{}\}  {}\mrightarrow{}  \mBbbR{}
4.  y  :  \{n..m  +  1\msupminus{}\}  {}\mrightarrow{}  \mBbbR{}
5.  i  :  \mBbbZ{}
6.  n  \mleq{}  i
7.  i  \mleq{}  m
\mvdash{}  |x[i]|  \mleq{}  (|x[i]  +  y[i]|  +  |y[i]|)


By

---

Latex:
(Assert  |y[i]|  =  |-(y[i])|  BY
              Auto)

---

Home Index