---

Step * 2 of Lemma qabs-qsum-qle


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)))
BY
{ (Auto THEN (InstHyp [⌜b - a⌝;⌜λ2i.E[a + i]⌝;⌜x⌝] 1⋅ THENA Auto)) }

1
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)
⊢ |Σa ≤ j < b. E[j]| ≤ ((b - a) * x)

---

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)
\mvdash{}  \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:
(Auto  THEN  (InstHyp  [\mkleeneopen{}b  -  a\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}i.E[a  +  i]\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]  1\mcdot{}  THENA  Auto))

---

Home Index