---

Step * of Lemma qabs-qsum-qle

∀[a,b:ℤ]. ∀[E:{a..b-} ⟶ ℚ]. ∀[x:ℚ].
  |Σa ≤ j < b. E[j]| ≤ ((b - a) * x) supposing (a ≤ b) ∧ (∀j:ℤ. ((a ≤ j) ⇒ j < b ⇒ (|E[j]| ≤ x)))
BY
{ Assert ⌜∀n:ℕ. ∀[E:ℕn ⟶ ℚ]. ∀[x:ℚ].  |Σ0 ≤ j < n. E[j]| ≤ (n * x) supposing ∀j:ℕn. (|E[j]| ≤ x)⌝⋅ }

1
.....assertion..... 
∀n:ℕ. ∀[E:ℕn ⟶ ℚ]. ∀[x:ℚ].  |Σ0 ≤ j < n. E[j]| ≤ (n * x) supposing ∀j:ℕn. (|E[j]| ≤ x)

2
1. ∀n:ℕ. ∀[E:ℕn ⟶ ℚ]. ∀[x:ℚ].  |Σ0 ≤ j < n. E[j]| ≤ (n * x) supposing ∀j:ℕn. (|E[j]| ≤ x)
⊢ ∀[a,b:ℤ]. ∀[E:{a..b-} ⟶ ℚ]. ∀[x:ℚ].
    |Σa ≤ j < b. E[j]| ≤ ((b - a) * x) supposing (a ≤ b) ∧ (∀j:ℤ. ((a ≤ j) ⇒ j < b ⇒ (|E[j]| ≤ x)))

---

Latex:

---

Latex:
\mforall{}[a,b:\mBbbZ{}].  \mforall{}[E:\{a..b\msupminus{}\}  {}\mrightarrow{}  \mBbbQ{}].  \mforall{}[x:\mBbbQ{}].
    |\mSigma{}a  \mleq{}  j  <  b.  E[j]|  \mleq{}  ((b  -  a)  *  x)  supposing  (a  \mleq{}  b)  \mwedge{}  (\mforall{}j:\mBbbZ{}.  ((a  \mleq{}  j)  {}\mRightarrow{}  j  <  b  {}\mRightarrow{}  (|E[j]|  \mleq{}  x)))


By

---

Latex:
Assert  \mkleeneopen{}\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)\mkleeneclose{}\mcdot{}

---

Home Index