Step
*
1
2
1
1
of Lemma
qabs-qsum-qle
1. n : ℤ
2. 0 < n
3. ∀[E:ℕn - 1 ⟶ ℚ]. ∀[x:ℚ]. |Σ0 ≤ j < n - 1. E[j]| ≤ ((n - 1) * x) supposing ∀j:ℕn - 1. (|E[j]| ≤ x)
4. E : ℕn ⟶ ℚ
5. x : ℚ
6. ∀j:ℕn. (|E[j]| ≤ x)
7. |Σ0 ≤ j < n - 1. E[j]| ≤ ((n - 1) * x)
⊢ |Σ0 ≤ j < n - 1. E[j] + E[n - 1]| ≤ (n * x)
BY
{ (RWW "q-triangle-inequality -1" 0 THENA Auto)⋅ }
1
1. n : ℤ
2. 0 < n
3. ∀[E:ℕn - 1 ⟶ ℚ]. ∀[x:ℚ]. |Σ0 ≤ j < n - 1. E[j]| ≤ ((n - 1) * x) supposing ∀j:ℕn - 1. (|E[j]| ≤ x)
4. E : ℕn ⟶ ℚ
5. x : ℚ
6. ∀j:ℕn. (|E[j]| ≤ x)
7. |Σ0 ≤ j < n - 1. E[j]| ≤ ((n - 1) * x)
⊢ (((n - 1) * x) + |E[n - 1]|) ≤ (n * x)
Latex:
Latex:
1. n : \mBbbZ{}
2. 0 < n
3. \mforall{}[E:\mBbbN{}n - 1 {}\mrightarrow{} \mBbbQ{}]. \mforall{}[x:\mBbbQ{}].
|\mSigma{}0 \mleq{} j < n - 1. E[j]| \mleq{} ((n - 1) * x) supposing \mforall{}j:\mBbbN{}n - 1. (|E[j]| \mleq{} x)
4. E : \mBbbN{}n {}\mrightarrow{} \mBbbQ{}
5. x : \mBbbQ{}
6. \mforall{}j:\mBbbN{}n. (|E[j]| \mleq{} x)
7. |\mSigma{}0 \mleq{} j < n - 1. E[j]| \mleq{} ((n - 1) * x)
\mvdash{} |\mSigma{}0 \mleq{} j < n - 1. E[j] + E[n - 1]| \mleq{} (n * x)
By
Latex:
(RWW "q-triangle-inequality -1" 0 THENA Auto)\mcdot{}
Home
Index