Step
*
1
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
8. |y[i]| = |-(y[i])|
⊢ |x[i]| ≤ (|x[i] + y[i]| + |y[i]|)
BY
{ (RWO "-1" 0 THENA 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
8. |y[i]| = |-(y[i])|
\mvdash{} |x[i]| \mleq{} (|x[i] + y[i]| + |y[i]|)
By
Latex:
(RWO "-1" 0 THENA Auto)
Home
Index