---

Step * 2 1 1 1 1 1 of Lemma qabs-qsum-qle


1. ∀n:ℕ. ∀[E:ℕn ⟶ ℚ]. ∀[x:ℚ].  |Σ0 ≤ j < n. E[j]| ≤ (n * x) supposing ∀j:ℕn. (|E[j]| ≤ x)
2. a : ℤ
3. b : ℤ
4. E : {a..b-} ⟶ ℚ
5. x : ℚ
6. a ≤ b
7. ∀j:ℤ. ((a ≤ j) ⇒ j < b ⇒ (|E[j]| ≤ x))
8. |Σ0 ≤ j < b - a. E[a + j]| ≤ ((b - a) * x)
9. Σa ≤ j < b. E[j] = Σa + (-a) ≤ j < b + (-a). E[j - -a] ∈ ℚ
⊢ Σa + (-a) ≤ j < b + (-a). E[j - -a] = Σ0 ≤ j < b - a. E[a + j] ∈ ℚ
BY
{ xxx(EqCD THEN Auto)xxx }

---

Latex:

---

Latex:

1.  \mforall{}n:\mBbbN{}.  \mforall{}[E:\mBbbN{}n  {}\mrightarrow{}  \mBbbQ{}].  \mforall{}[x:\mBbbQ{}].    |\mSigma{}0  \mleq{}  j  <  n.  E[j]|  \mleq{}  (n  *  x)  supposing  \mforall{}j:\mBbbN{}n.  (|E[j]|  \mleq{}  x)
2.  a  :  \mBbbZ{}
3.  b  :  \mBbbZ{}
4.  E  :  \{a..b\msupminus{}\}  {}\mrightarrow{}  \mBbbQ{}
5.  x  :  \mBbbQ{}
6.  a  \mleq{}  b
7.  \mforall{}j:\mBbbZ{}.  ((a  \mleq{}  j)  {}\mRightarrow{}  j  <  b  {}\mRightarrow{}  (|E[j]|  \mleq{}  x))
8.  |\mSigma{}0  \mleq{}  j  <  b  -  a.  E[a  +  j]|  \mleq{}  ((b  -  a)  *  x)
9.  \mSigma{}a  \mleq{}  j  <  b.  E[j]  =  \mSigma{}a  +  (-a)  \mleq{}  j  <  b  +  (-a).  E[j  -  -a]
\mvdash{}  \mSigma{}a  +  (-a)  \mleq{}  j  <  b  +  (-a).  E[j  -  -a]  =  \mSigma{}0  \mleq{}  j  <  b  -  a.  E[a  +  j]


By

---

Latex:
xxx(EqCD  THEN  Auto)xxx

---

Home Index